diff --git a/VERSION b/VERSION
index 8f08de2f1dcbcd644edd53ebb9dbf9ce6bb2f9e9..e05f67667f953aef068e3ff9bf4a4244478e7463 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-19.0-beta
\ No newline at end of file
+19.0-beta2
\ No newline at end of file
diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex
index 0d6b3898b618e4e448498e3b2c466cdee5e47b19..3339418d818c888eacdd9f57f0137d9c3118a831 100644
--- a/doc/userman/user-start.tex
+++ b/doc/userman/user-start.tex
@@ -71,9 +71,12 @@ may be found in the file \texttt{INSTALL.md} of the source distribution.
\item \texttt{frama-c.byte}\codeidx{frama-c.byte}: bytecode batch version;
\item \texttt{frama-c-gui}\codeidx{frama-c-gui}: natively-compiled interactive
version;
-\item \texttt{frama-c-gui.byte}\codeidx{frama-c-gui.byte}: bytecode interactive version.
+\item \texttt{frama-c-gui.byte}\codeidx{frama-c-gui.byte}: bytecode interactive version;
\item \texttt{frama-c-config}\codeidx{frama-c-config}: auxiliary batch version for
- quickly retrieving configuration information (e.g. installation path).
+ quickly retrieving configuration information (e.g. installation path);
+\item \texttt{frama-c-script}\codeidx{frama-c-script}: contains several
+ utilities related to source preparation, results visualization and analysis
+ automation. Run it without arguments to obtain more details.
\end{itemize}
The differences between these versions are described below.
\begin{description}
diff --git a/doc/userman/userman.bib b/doc/userman/userman.bib
index a8abde0581e886288dc4526765a1013c7ad2d742..2c1e9cc7f4f628618a850338cda4a1f7d2aec884 100644
--- a/doc/userman/userman.bib
+++ b/doc/userman/userman.bib
@@ -1,5 +1,5 @@
@manual{plugin-dev-guide,
- author = {Julien Signoles and Loïc Correnson and Matthieu Lemerre and
+ author = {Julien Signoles and Thibaud Antignac and Loïc Correnson and Matthieu Lemerre and
Virgile Prevosto},
title = {{Frama-C Plug-in Development Guide}},
year = 2015,
diff --git a/doc/value/biblio.bib b/doc/value/biblio.bib
index 7d4b23fa8933126b3c5b910429a35b3266274136..afdbbf9218d7537cce903dde676973f4b123dbb2 100644
--- a/doc/value/biblio.bib
+++ b/doc/value/biblio.bib
@@ -73,6 +73,14 @@
organization = {CEA, List},
note = {Available at \url{https://frama-c.com/download/frama-c-user-manual.pdf}}}
+@manual{plugin-dev-guide,
+ author = {Julien Signoles and Thibaud Antignac and Loïc Correnson and Matthieu Lemerre and
+ Virgile Prevosto},
+ title = {{Frama-C Plug-in Development Guide}},
+ year = 2015,
+ month = feb,
+ note = {\newline \url{http://frama-c.com/download/frama-c-plugin-development-guide.pdf}},
+}
@inproceedings{DBLP:conf/sas/JacqueminPV18,
author = {Maxime Jacquemin and
diff --git a/doc/value/gui-loop-to-unroll.png b/doc/value/gui-loop-to-unroll.png
new file mode 100644
index 0000000000000000000000000000000000000000..815f58b3950025b6d61cc4c8ddd3891b9a302b8a
Binary files /dev/null and b/doc/value/gui-loop-to-unroll.png differ
diff --git a/doc/value/gui.tex b/doc/value/gui.tex
index 1b15f138f9080035a32172dd5c4dbe6fa7c46e9b..62e1b8e87129388ad83eb8baecb4e56d81355141 100644
--- a/doc/value/gui.tex
+++ b/doc/value/gui.tex
@@ -21,7 +21,7 @@ As a general recommendation,
\Eva{} does not use the GUI for anything else other than rendering its
results. It is recommended to run the value analysis using the command line,
and then saving the result to a Frama-C save file
- (see Section~\ref{saving-result}).
+ (see Section~\ref{three-step}).
\section{A general view of the GUI}
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 15d5553fb0a48ebc63c5c0bc8f0ab51525505895..a541d32a9a709ff3c1bd5e5deb9856acf1a749ae 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -3,6 +3,7 @@
\usepackage{microtype}
\usepackage{lmodern}
\usepackage{booktabs}
+\usepackage{calc}
% Commandes pour mettre des ref dans l'index :
\newcommand{\idb}[1]{\textbf{#1}}
@@ -17,6 +18,17 @@
\newcommand{\cbopen}{\mbox{\tt \{}}
\newcommand{\cbclose}{\mbox{\tt \}}}
+% Special environment
+\definecolor{gris}{gray}{0.85}
+
+\makeatletter
+\newenvironment{important}%
+{\hspace{5pt plus \linewidth minus \marginparsep}%
+ \begin{lrbox}{\@tempboxa}%
+ \begin{minipage}{\linewidth - 2\fboxsep}\itshape}
+{\end{minipage}\end{lrbox}\colorbox{gris}{\usebox{\@tempboxa}}}
+\makeatother
+
\newcommand{\framacversion}%
{\input{../../VERSION} (\input{../../VERSION_CODENAME}\unskip)}
@@ -144,7 +156,7 @@ invalid pointer accesses,\ldots
When launched with \lstinline|frama-c -eva rte.c|,
\Eva{} emits a warning about an out-of-bound access at line 5:
\begin{logs}
-rte.c:5:[kernel] warning: accessing out of bounds index. assert i < 10;
+[eva:alarm] rte.c:5: Warning: accessing out of bounds index. assert i < 10;
\end{logs}
There is in fact an out-of-bounds access at this line in the program.
It can also happen that, because of approximations during its computations,
@@ -289,16 +301,16 @@ After extracting the archive \lstinline|skein_NIST_CD_010509.zip|,
listing the files in\\
\lstinline|NIST/CD/Reference_Implementation| shows:
\begin{listing}{1}
--rw-r--r-- 1 pascal 501 4984 Oct 14 00:52 SHA3api_ref.c
--rw-r--r-- 1 pascal 501 2001 Oct 14 00:54 SHA3api_ref.h
--rw-r--r-- 1 pascal 501 6141 Sep 30 00:28 brg_endian.h
--rw-r--r-- 1 pascal 501 6921 May 17 2008 brg_types.h
--rw-r--r-- 1 pascal 501 34990 Jan 6 01:39 skein.c
--rw-r--r-- 1 pascal 501 16290 Nov 9 05:48 skein.h
--rw-r--r-- 1 pascal 501 18548 Oct 7 20:02 skein_block.c
--rw-r--r-- 1 pascal 501 7807 Oct 10 02:47 skein_debug.c
--rw-r--r-- 1 pascal 501 2646 Oct 9 23:44 skein_debug.h
--rw-r--r-- 1 pascal 501 1688 Jul 3 2008 skein_port.h
+SHA3api_ref.c
+SHA3api_ref.h
+brg_endian.h
+brg_types.h
+skein.c
+skein.h
+skein_block.c
+skein_debug.c
+skein_debug.h
+skein_port.h
\end{listing}
The most natural place to go next is the file \lstinline|skein.h|,
@@ -339,7 +351,7 @@ use string-printing functions, hence the \lstinline|for| loop at lines 17-18.
\goodbreak
With luck, the compilation goes smoothly and we obtain
-the hash value:
+a hash value:
\begin{shell}
gcc *.c
./a.out
@@ -356,13 +368,18 @@ gcc *.c
13
\end{logs}
+\begin{important}
+ Your actual result may differ from the one above;
+ this will be explained later.
+\end{important}
+
\subsection{First try at an analysis using \Eva{}}
Let us now see how \Eva{} works on the same example.
\Eva{} can be launched with the following command.
The analysis should not take more than a few seconds:
\begin{listing-nonumber}
-frama-c -eva *.c >log
+frama-c -eva main_1.c >log
\end{listing-nonumber}
Frama-C has its own model of the target platform (the default target is
@@ -393,17 +410,23 @@ to send it to a log file.
There is also a Graphical User Interface
for creating analysis projects and
visualizing the results.
-The GUI is still evolving quickly at this stage
-and it would not make much sense to
-describe its manipulation in detail in this document.
-You are however encouraged to try it if it is available on your
-platform.
+Note that you cannot {\em edit} the source code in the GUI, only visualize it.
+Most of the information present in the console is also available in the GUI,
+but presented differently. Each interface (terminal or GUI) is better suited
+for a specific set of tasks.
+
One way to create an analysis project in the GUI
is to pass the command \lstinline|frama-c-gui| the same options
that would be passed to \lstinline|frama-c|. In this first example,
-the command \lstinline|frama-c-gui -eva *.c| launches
+the command \lstinline|frama-c-gui -eva main_1.c| launches
the same analysis and then opens the GUI for inspection of the results.
+\begin{important}
+ For simple projects like this tutorial, running everything at once
+ is perfectly suitable; however, for larger analyses, we recommend the
+ three-step approach presented in section~\ref{three-step}.
+\end{important}
+
The initial syntactic analysis and symbolic link phases
of Frama-C may find issues such as
inconsistent types for the same symbol in different files.
@@ -417,7 +440,7 @@ lines of the log.
Since we are trying out the library for the first time,
something else to look for in the log file is the list of functions for
which the source code is missing. \Eva{} requires
-either a body or a specification for each function it analyses.
+either a body or a specification for each function it analyzes.
\begin{listing-nonumber}
grep "Neither code nor specification" log
@@ -425,48 +448,74 @@ grep "Neither code nor specification" log
This should match lines indicating functions that are both undefined
(without source) and that have no specification in Frama-C's standard library.
-In this example, no functions will be output, since Frama-C's standard library
-already has prototypes for the most important library functions.
-
-But suppose you would have a custom printing
-function, say \verb|print| instead of \verb|printf|, or some other function
-with missing source code. For instance, change the code in \verb|main_1.c|,
-replacing \verb|printf| with \verb|print|, re-run \Eva{},
-and then grep the log again. You will obtain this output:
+In our example, we obtain the following lines in the log:
\begin{logs}
-main_1.c:14:[kernel] warning: Neither code nor specification for function print,
+[kernel:annot:missing-spec] main_1.c:13: Warning:
+ Neither code nor specification for function Skein_256_Init,
generating default assigns from the prototype
+[eva] using specification for function Skein_256_Init
\end{logs}
-The warning indicates that \Eva{} is trying to infer an
-{\em assigns} clause for the function. This will be explained in detail later
-(\ref{annot_assigns}), but for now the important part is that \Eva{}
-needs either source code or an ACSL specification in order to work.
-Without those, it can only guess what each function does from the function's
-prototype, which is both inaccurate and likely incorrect.
+The same messages are produced for functions \verb|Skein_256_Update| and
+\verb|Skein_256_Final|.
+For each function, there are two messages: first, a warning about the absence
+of either code or ACSL specification for the function, stating
+that an {\em assigns} clause will be generated for the function
+(the {\em assigns} clause will be explained in detail later, in
+section~\ref{annot_assigns}). Second, a message stating that \Eva{} will use a
+specification for the missing function.
+
+What happens is that, without code or specification, Frama-C can only
+{\em guess} what each function does from the function's prototype,
+which is both inaccurate and likely incorrect. \Eva{} needs a specification
+for each function without body reached during the analysis, so one is created
+on the fly and then used, but results are likely to be unsatisfactory.
+
+\begin{important}
+ Absence of code or ACSL specification is a major issue which often renders
+ the analysis incorrect. For this reason, we recommend converting this warning
+ into an error, in order to spot it immediately.
+ The {\em analysis script templates}, to be presented in
+ section~\ref{analysis-scripts}, already include this change.
+\end{important}
+
+To fix the issue, we only need to give Frama-C all of the C sources in
+the directory:
+\begin{listing-nonumber}
+frama-c -eva *.c >log
+\end{listing-nonumber}
-Once we are convinced that all functions have either a body or a specification,
-we can focus on functions without bodies:
+No further warnings about missing functions are emitted. We can now focus on
+functions without bodies:
\begin{listing-nonumber}
grep "using specification for function" log
-[eva] using specification for function memset
-[eva] using specification for function memcpy
-[eva] using specification for function printf
+[eva] using specification for function printf_va_1
\end{listing-nonumber}
-We find three functions. Not having a body for \verb|printf| is fine,
-since calls to this function have no observable effects for the analysis.
-Things are not so clear-cut for
-\verb|memcpy| and \verb|memset|, for which we will provide bodies later.
+This \verb|printf_va_1| function is not present directly in the source code;
+it is a specialization of a call to the variadic function \verb|printf|. This
+specialization is performed by the \textsf{Variadic} plugin\footnote{The
+ \textsf{Variadic} plugin is described in more detail in the Frama-C User
+ Manual~\cite{FCUserMan}.}.
+All we need to know for now is that the plugin handles calls to variadic functions
+and produces sound specifications for them, which are then used by \Eva{}.
+This call to \verb|printf| has no observable effects for the analysis anyway,
+so we do not have anything to be concerned with. It is still a good idea to
+check the specification of each function without body used during the analysis,
+since the overall correctness depends on them. This can be done using the
+GUI or, in the command line, with option \verb|-print|, which outputs the
+Frama-C normalized source code, including ACSL specifications and
+transformations performed by the \textsf{Variadic} plugin.
It is also possible to obtain a list of
missing function definitions by using the command:
\begin{listing-nonumber}
-frama-c -metrics -metrics-libc *.c
+frama-c -metrics *.c
\end{listing-nonumber}
This command computes, among other pieces of information,
-a list of missing functions using
-a syntactic analysis. It is not exactly equivalent to
+a list of missing functions (under the listing ``Undefined functions'')
+using a syntactic analysis produced by the \textsf{Metrics} plugin.
+It is not exactly equivalent to
grepping the log of \Eva{} because it lists
all the functions that are missing, while the log of
\Eva{} only cites the functions that would have
@@ -477,93 +526,65 @@ In this case, relying on the information displayed by \lstinline|-metrics|
means spending time hunting for functions that are not actually
necessary.
-
-The output of \verb|frama-c -metrics -metrics-libc *.c|
-will then include the following lines:
+By default, \textsf{Metrics} does not list functions from the standard C
+library. This can be done by adding option \verb|-metrics-libc|, which would
+produce something similar to:
\begin{logs}
-Undefined functions (83)
+Undefined functions (90)
=======================
[...]
- gets (0 call); memchr (0 call); memcmp (0 call); memcpy (21 calls);
- memmove (0 call); memset (27 calls); perror (0 call); printf (1 call)
+memcpy (21 calls); memmove (0 call); memset (27 calls); pclose (0 call);
+perror (0 call); popen (0 call); printf_va_1 (1 call); putc (0 call);
\end{logs}
-All functions included from \verb+string.h+ are undefined, but only
-\verb+memcpy+, \verb+memset+ and \verb+printf+ are called.
-
-
-To handle the absence of functions \lstinline|memset| and \lstinline|memcpy|%
-\footnote{Since \FramaC 18 (Argon), \Eva{} includes builtin functions for
- \lstinline|memset| and \lstinline|memcpy|,
- thus providing source code for them is no longer necessary.},
-we will provide source code for them.
-Sometimes it is a good idea to provide the
-exact source code that will actually be used in an actual
-running environment, so as to detect subtle bugs in the interactions
-between the program and the system libraries.
-On the other hand, string manipulation functions often
-feature difficult-to-analyze
-architecture-dependent optimizations.
-For these, it is better to provide a simpler but equivalent implementation.
-In this particular case, let us provide these two
-functions in a file that we will place with the others and
-name ``\lstinline|lib.c|''.
-\listinginput{1}{tutorial/lib.c}
-
-%% Some compilation platforms' headers define the names \lstinline|memset|
-%% and \lstinline|memcpy| in ways that make it impossible to provide
-%% your own implementation for these functions. If this happens for
-%% yours, you can try placing your own header in the analysis directory,
-%% under the name ``\lstinline|string.h|''
-%% \listinginput{1}{tutorial/string.h}
-
-%% In some circumstances, the results of \Eva{} may
-%% remain useful even when letting Frama-C guess the effects
-%% of missing functions. In the case of functions that take
-%% pointers as arguments, however, the possibilities are too numerous
-%% for the analyzer to be able to guess right.
-%% In this example, the function \lstinline|printf| is safe to
-%% leave without an implementation, because
-%% unlike the other two,
-%% it does not have effects on the variables of the program.
-
-%. It is generally far simpler to provide
-%either the actual code or a model written in C
-%for the missing functions.
-
-For some functions -- including those two -- an implementation is
-already provided in \FramaC. It can be found in the \lstinline|.c|
-files of the directory \lstinline|share/frama-c/libc|, usually within
-a file identically named to the header declaring the functions. For
-\lstinline|memcpy| and \lstinline|memset|, the implementation can thus
-be found in \lstinline|string.c|, and adding it to the list of files
-to be analyzed would make the warning disappear.
-%
-However, we are going to assume that such implementations are not available
-in the remainder of this tutorial. Since quite a few functions do not have
-any implementation in \FramaC's \lstinline|libc|, this allows us to show how
-to deal with the general case.
-
-\subsection{First meaningful analysis}
-
-If we run the analysis again with definitions for \lstinline|memset|
-and \lstinline|memcpy|, the newly obtained log no longer mentions
-any missing function other than \lstinline|printf|\footnote{It is
-a good idea to
-check again for missing functions because new execution paths
-could have been activated by the implementations of functions
-that were previously missing.}.
-
-The log next contains a description of the initial values of
-variables. Apart from the variables that we defined ourselves, there
-is a rather strange one, named \lstinline|ONE| and indeed containing
+Besides \verb|printf_va_1|, only functions \verb|memcpy| and \verb|memset|
+are called. These functions are already specified in the Frama-C libc. However,
+when running \Eva{}, they result in an output similar to the following:
+
+\begin{logs}
+[eva] FRAMAC_SHARE/libc/string.h:118:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
+\end{logs}
+
+Note that this message is {\em not} a warning (it does not begin with the word
+``Warning'') neither an alarm (it is not prefixed with \verb|[eva:alarm]|). It
+is an informative message related to Frama-C's libc specifications that can be
+safely ignored\footnote{For the interested reader:
+ some of the more thorough ACSL specifications in Frama-C's
+ \texttt{<string.h>} are useful for plugins such as \textsf{WP},
+ but are not yet fully interpreted by \Eva{}. Instead, \Eva{} has builtins to
+ correctly interpret these libc functions without only relying on their
+ specification.}
+and will likely disappear in future Frama-C releases.
+
+\subsection{Interpreting the output of the analysis}
+
+By default, \Eva{}'s log emits several messages during the analysis, which are
+essential for a deep understanding of the issues which may happen, but on
+overview, these are the main components of the log:
+
+\begin{itemize}
+\item parsing and related messages (in our case, simply the list of files being
+ parsed);
+\item start of the analysis by \Eva{}, with the initial values of global
+ variables;
+\item messages emitted during the analysis, such as warnings, alarms and
+ informative feedback;
+\item values for all variables at the end of each function;
+\item an analysis summary, with coverage and the number of
+ errors, warnings, alarms and logical properties.
+\end{itemize}
+
+If we focus on the initial values of variables, we notice that,
+apart from the variables defined in the source code, there
+is a rather strange variable named \lstinline|Skein_Swap64_ONE| and containing
\lstinline|1|. Searching the source code reveals that this variable is
-in fact declared \lstinline|static| as it should be. Frama-C can
-display the value of static variables (something that is annoying to
-do when using a C compiler for testing). Frama-C may rename
-static variables in order to distinguish them from another variable
-with the same name. The GUI displays the original source code
-alongside the transformed one.
+in fact variable \verb|ONE|, declared \lstinline|static| inside function
+\lstinline|Skein_Swap64|. Frama-C can
+display the value of static variables, something that is annoying to
+do when using a C compiler for testing.
+The GUI displays the original source code alongside the transformed one,
+and allows navigating between uses of a variable and its declaration.
A quick inspection shows that the Skein functions
use variable \lstinline|ONE| to detect endianness.
@@ -576,259 +597,236 @@ The big-endian version of the library could be analyzed
by reproducing the same steps we are taking here for
a big-endian configuration of Frama-C.
-You will also see lots of variable names
+You may also see variable names
prefixed by \verb|__fc_|, \verb|__FC_| and \verb|S___fc_|.
-These are all variables coming from ACSL specifications in the Frama-C
+These are variables coming from ACSL specifications in the Frama-C
standard library.
-The next line in the log is a progression message, that indicates
-that \Eva{} has encountered a loop and is performing an approximations.
-Those messages can be ignored for now.
-\begin{logs}
-lib.c:17:[eva] entering loop for the first time
-\end{logs}
+After the initial values, the analysis log contains some lines such as:
-The next log entry which is not a progression message is a
-warning concerning variable \lstinline|tmp|
\begin{logs}
-lib.c:18:[kernel] warning: out of bounds write. assert \valid(tmp);
- (tmp from ptr++)
+[eva] skein_block.c:56: starting to merge loop iterations
\end{logs}
-There is no variable \lstinline|tmp| in our file \lstinline|lib.c|,
-but as indicated in the message, this variable is introduced by the source
-code normalization of the \verb|ptr++| expression.
-You can also see the relation between this variable
-and the original source code in the GUI.
-Alternately, the command \lstinline|frama-c *.c -print|
-shows how the original source code has been
-transformed by Frama-C (note, however, that the location
-\lstinline|lib.c:18| refers to the original source file).
-Here, it is the statement \lstinline|*ptr++ = val;| in the
-function \lstinline|memset| that has been transformed by
-Frama-C into the sequence below, so that it would not
-be ambiguous which value of \lstinline|ptr|
-has to be a valid pointer.
-\begin{listing-nonumber}
- tmp = ptr;
- ptr ++;
- *tmp = (unsigned char)val;
-\end{listing-nonumber}
+This means that \Eva{} has encountered a loop and is performing an
+approximation. These messages can be ignored for now.
-The command \lstinline|frama-c *.c -eva -print| launches
-\Eva{} and then prints the transformed source code,
-annotated with the
-alarms raised by \Eva{}. In our case, the
-function \lstinline|memset| is transformed in
-\begin{listing-nonumber}
-void *memset(void *dest, int val, size_t len)
-{
- unsigned char *ptr;
- ptr = (unsigned char *)dest;
- while (1) {
- size_t tmp_0;
- unsigned char *tmp;
- { /* sequence */
- tmp_0 = len;
- len --;
- ;
- }
- if (! (tmp_0 > (size_t)0)) break;
- { /* sequence */
- tmp = ptr;
- ptr ++;
- /*@ assert Value: mem_access: \valid(tmp); */
- *tmp = (unsigned char)val;
- }
- }
- return dest;
-}
-\end{listing-nonumber}
+Arguably some of the most important messages in the analysis are {\em alarms},
+such as the one below:
+
+\begin{logs}
+[eva:alarm] skein_block.c:69: Warning:
+ accessing uninitialized left-value. assert \initialized(&ks[i]);
+\end{logs}
As we will find out later in this tutorial, this alarm is a false
alarm, an indication of a potential problem in a place where there is
-in fact none. On the other hand, \Eva{} never remains
+in fact none. However, \Eva{} never remains
silent when a risk of run-time error is present, unlike many other
static analysis tools. The important consequence is that if you get
the tool to remain silent, you have {\em formally verified} that
no run-time error could happen when running the program.
-
-It may seem that the access to \lstinline|*tmp| is the
-only dangerous operation in the function \lstinline|memset|,
-and therefore that the analyzer is not doing a very good job
-of pointing only the operations that are problematic.
-While it is true that the results obtained on this example
-are not very precise, the comparison
-\lstinline|>| is also considered dangerous
-by the analyzer. This operation may be unspecified when applied
-to an invalid pointer. Consider a program that does the
-following:
-\begin{listing}{1}
-int main()
-{
- int a;
- return ((unsigned int)(&a - 1432)) > 0;
-}
-\end{listing}
-The programmer might misguidedly have written the \lstinline|>0|
-test in this example as a way to test for \lstinline|NULL|.
-Ey\footnote{This manual uses Spivak pronouns:
-\url{http://en.wikipedia.org/wiki/Spivak_pronoun}} might
-expect this program always to return 1, since
-\lstinline|(&a - 1432)| is not \lstinline|NULL|. But this
-program may in fact return 0 if, out of bad luck,
-the compiler places variable \lstinline|a| precisely at address
-1432. This kind of bug would be very
-difficult to find and/or reproduce by testing.
-
-The analyzer does not emit any alarm for the comparison
-\lstinline|tmp_0 > (size_t )0| in the normalized source code
-for \lstinline|memset|, and
-this means that it guarantees\footnote{The fine print is
-the reference part of this manual} that
-this particular comparison is never non-deterministic
-because of an issue such as the one just described.
-This conclusion can only be reached by looking at
-the arguments actually passed to the function \lstinline|memset|.
-Therefore, this conclusion is only valid for all the
-possible executions coming from the \lstinline|main|
-function that we provided, and not for all the possible
-calls to function \lstinline|memset| that a programmer
-could write.
-
-One should not spend too much time at this stage trying to
-determine if the dozens or so alarms emitted by the analyzer
-are true alarms that indicate an actual problem or false alarms
-that don't.
-The most important information is that the analysis did not
-take an unreasonable time.
-% The second most important information is that the analysis
-% seems to have explored all the paths we intended for it to
-% explore, as seen in the list of functions for which values are
-% printed or in the log entries such as:
-% \begin{logs}
-% [value] computing for function RotL_64 <- Skein_256_Process_Block
-% <- Skein_256_Final <- main.
-% Called from skein_block.c:100.
-% \end{logs}
-
-The GUI allows to inspect the sets of values
-obtained during the analysis and to get
-a feeling of how it works. Right-clicking on the function name
-in a function call brings a contextual menu that allows to go
-to the function's definition and to inspect it in turn.
-In order to return to the caller,
-right-clicking on the name of the current function at the top
-of the normalized code buffer brings a contextual menu
-with a list of callers.
-You can also use the Back button (left arrow) in the toolbar.
-\section{Searching for bugs}
+The alarm means that \Eva{} could not prove that the value \verb|ks[i]|
+accessed in \verb|skein_block.c:69| was definitely initialized before being
+read. Reading an initialized value is an undefined behavior according to the
+ISO C99 standard (and can even lead to security vulnerabilities).
-\subsection{Increasing the precision with option {\tt -eva-slevel}}
+As is often the case, this alarm is related to the approximation introduced
+in \verb|skein_block.c:56|, which is the loop responsible for initializing
+the values of array \verb|ks[i]|. The order of the messages during the
+analysis thus provides some hints about what is happening, and also some
+ideas about how to solve them.
-Because we compiled and executed the same program that we are
-now analyzing, we are confident that most of the alarms
-displayed by \Eva{} are false alarms that do not
-correspond to actual problems. In fact, because the program
-is deterministic and takes no inputs,
-only one of the alarms can be a true alarm in
-the strictest sense. The analysis stops when an error is
-encountered (what would it even mean to continue the analysis
-after, for instance, \lstinline|NULL| has been dereferenced?).
-It is only because \Eva{} is uncertain about the errors
-encountered here that it continues and finds more possible
-errors.
+\subsection{Increasing analysis precision in loops}
+The previous alarm is just one of several related to variable initialization.
Before we spend any of our time looking at each of these alarms,
-trying to determine whether it is true or false,
-it is a good idea to make the analyzer spend more of its time
-trying to determine whether each alarm is true or false.
+trying to determine whether they are true or false,
+it is a good idea to make the analyzer spend more of {\em its} time
+trying to determine the same thing.
There are different settings that influence the compromise
-between precision and resource consumption.
-If you chose to remember only one of these settings, it would
-have to be the option \lstinline|-eva-slevel|. This option has
-two visible effects:
-it makes the analyzer unroll loops, and it makes it propagate
-separately the states that come from the \lstinline|then|
-and \lstinline|else| branches of a conditional statement.
-This makes the analysis more precise (at the cost of being
-slower) for almost every program that can be analyzed.
-
-\Eva{} has different ways to provide information on
-the loss of precision that causes the false alarms.
-This is another reason why it is so verbose during an analysis:
-it tries to provide enough information for a motivated user
-to be able to understand what is happening during the analysis,
-where the imprecise values that cause the false alarms came from,
-and what instructions in the program made them imprecise.
-
-But instead of spending precious human time making use
-of the provided information, the brute-force approach of blindly
-applying the \lstinline|-eva-slevel| option must be tried first.
-Indeed, \lstinline|-eva-slevel| is one of the options of \Eva{}
-that can never cause it to become incorrect. Such options,
-when used wrongly, may make the analysis slower,
-provide hints that are not
-useful, or even possibly counter-productive (making the analysis
-less precise), but they cannot
-prevent the analyzer from reporting a problem where there is one.
-
-The \lstinline|-eva-slevel| option is useful for unrolling loops. We do
-not know without further inspection how many iterations the loops
-inside the program need, but the input message is 80 characters long,
-and we can assume that it is read inside a loop, so using the option
-\lstinline|-eva-slevel 100| should have a good chance of unrolling at
-least that loop. Furthermore, it does not make the analysis slower to
-use a number greater than the value actually necessary to unroll
-every loop and conditional in the program. We are limiting ourselves
-to 100 in this first try because we do not know how much time the
-analysis will take with this number of unrolled branches. If, with
-the parameter \lstinline|-eva-slevel 100|, the precision of the analysis still isn't
-satisfactory and the time spent by the analyzer remains reasonable, we
-can always try a higher value. This should be progressive, because a value
-higher than a few hundreds, when there really are that many branches to
-unroll in the program, can make the analysis very slow.
+between precision and resource consumption. When dealing with bounded loops,
+the best approach consists in using an ACSL annotation, \verb+//@ loop unroll N+,
+to direct \Eva{} to analyze precisely the N first iterations of the loop
+before approximating the results.
+
+Currently, annotating loops is done manually; in future releases of Frama-C,
+this will be partly automated. In simple loops, you can obtain its
+bounds via the GUI, by inspecting the values taken by the loop counter,
+as in the example below:
+
+\begin{figure}[hbt]
+\centering
+\includegraphics[width=0.75\textwidth]{gui-loop-to-unroll.png}
+\caption{Estimating loop unroll bounds in the GUI}
+\label{fig:gui-loop-to-unroll}
+\end{figure}
+
+In this case, \verb|WCNT| has a constant value (4), so it could also be used
+to estimate the loop bounds.
+
+We can then Ctrl+click on the loop condition in the original source view
+(right panel) to open an editor\footnote{The external code editor used by the GUI
+ can be defined via the menu {\em File - Preferences}.} centered on the loop, and
+then add the loop unroll annotation, as follows:
+
+\begin{lstlisting}
+ //@ loop unroll 4;
+ for (i=0;i < WCNT; i++)
+ {
+ ks[i] = ctx->X[i];
+ ks[WCNT] ^= ctx->X[i]; /* compute overall parity */
+ }
+\end{lstlisting}
+
+The value 4 is sufficient to completely unroll the loop, even though \verb|i|
+ranges from 0 to 4 (5 values in total). One way to confirm the unrolling is
+complete is to check that the ``starting to merge loop iterations'' is no
+longer emitted when entering the loop. Also, when a loop unroll annotation
+is present but insufficient to unroll the loop, a message is emitted:
+
+\begin{logs}
+[eva:loop-unroll] skein_block.c:57: loop not completely unrolled
+\end{logs}
+
+Once a loop is completely unrolled, any ``leftovers'' are ignored, so it incurs
+no extra cost. Using a value larger than necessary is therefore not an issue.
+
+The practical effect of adding this annotation and then re-running \Eva{} is
+the elimination of 3 alarms in the analysis. Thanks to the extra precision
+allowed by the annotation (with a minimal increase in analysis time), \Eva{}
+is now able to prove there are no initialization errors in more places than
+before.
+
+\subsection{Increasing precision}
+
+Option \verb|-eva-precision| allows setting a global trade-off between
+precision and analysis time. By default, \Eva{} is tuned to a low precision
+to ensure a fast initial analysis. Especially for smaller code bases, it is
+often useful to increase this precision, to dismiss ``easy'' alarms.
+Precision can be set between 0 and 11, the higher the value, the more precise
+the analysis. The default value of \Eva{} is somewhere between 0 and 1, so that
+setting \verb|-eva-precision 0| potentially allows it to go even faster
+(only useful for large or very complex code bases).
+
+\verb|-eva-precision| is in fact a meta-option, whose only purpose is to set
+the values of other options to a set of predefined values. This avoids the user
+having to know all of them, and which values are reasonable. Think of it as a
+``knob'' to perform a coarse adjustment of the analysis, before fine-tuning
+it more precisely with other options.
+
+\verb|-eva-precision| displays a message when it is used, stating which options
+are affected and the value given to them. If one of those options is already
+specified by the user, that value takes priority over the one chosen by
+\verb|-eva-precision|.
+
+Among the options set by \verb|-eva-precision|, there is \verb|-eva-slevel|,
+which can be thought of as some kind of ``fuel''
+to be consumed during the analysis: as long as there is some slevel,
+the analysis will keep states separated and maintain precision at the cost of
+extra analysis time; when all of
+it is consumed, further states are merged, avoiding increase in analysis time
+but approximating the results. It can also be
+specified separately for each function (\verb|-eva-slevel-function f:n|).
+
+For complex code bases, however, \verb|-eva-slevel| lacks in stability and
+predictability: it is very hard to determine exactly {\em how} it is used.
+It can be consumed in the presence of loops, branches, disjunctions;
+in nested loops, it is consumed by both inner and outer loops.
+In loops with branches, its consumption may become exponential.
+And once a satisfactory value is found, later changes to the source code,
+ACSL specifications, \Eva{}'s algorithms or other parameters can affect it,
+requiring a new parametrization.
+
+In our example, we can quickly try a few values of \verb|-eva-precision|,
+such as 1, 2 and 3:
\begin{shell}
-frama-c -eva-slevel 100 -eva *.c >log
+frama-c -eva-precision 3 -eva *.c >log
\end{shell}
-The analysis goes rather far without finding any alarm,
+Now, the analysis goes rather far without finding any alarm,
but when it is almost done (after the analysis of function
\lstinline|Skein_256_Final|), it produces:
\begin{logs}
...
-main_1.c:14:[kernel] warning: Neither code nor specification for function printf,
- generating default assigns from the prototype
-[eva] using specification for function printf
-[eva] Done for function printf
-main_1.c:14:[eva] completely invalid value in evaluation of
- argument (int)hash[i]
-main_1.c:14:[kernel] warning: accessing uninitialized left-value.
- assert \initialized(&hash[i]);
-[eva] Recording results for main
+[eva] using specification for function printf_va_1
+[eva:alarm] main_1.c:17: Warning:
+ accessing uninitialized left-value. assert \initialized(&hash[i]);
[eva] done for function main
...
\end{logs}
-These messages mean that lvalue \lstinline|hash[i]|, as found
-in line 14 of our file \lstinline|main_1.c|, may be
-uninitialized\footnote{An lvalue is a C expression that exists in memory.
-Examples of lvalues are a simple variable {\tt x}, the cell of an
-array {\tt t[i]}, or a pointed location {\tt *p}. Because an lvalue
-lies in memory, it may have uninitialized contents.
-Using an
-lvalue when it has not yet been initialized is a forbidden
-behavior that compilers do not detect in all cases, and this
-is only one of the numerous pitfalls of C.}.
-Actually, the analyzer finds that for one execution
-branch, it is certain to be uninitialized. This is when reading
-the memory location ``\lstinline|hash[i]|'', one of the arguments given
-to the \lstinline|printf| function.
-Extra information can be observed using the GUI, by clicking on the
-\lstinline|hash| expression in line 14 and reading the \textsf{Values} tab,
-which displays the following values for \lstinline|hash|:
+There remains an alarm about initialization, but all the others have been
+removed. Trying larger values for precision or slevel does not change this.
+In this case, we can afford to spend some time looking at it in more detail.
+
+\subsection{Inspecting alarms in the GUI}
+
+Instead of running \verb|frama-c|, let us use \verb|frama-c-gui|:
+
+\begin{shell}
+frama-c-gui -eva-precision 3 -eva *.c >log
+\end{shell}
+
+The GUI allows the user to navigate the source code, to inspect the sets of
+values inferred by the analysis and to get
+a feeling of how it works. Right-clicking on the function name
+at a call site brings a contextual menu to jump
+to the function's definition.
+In order to return to the caller,
+right-clicking on the name of the current function at the top
+brings a contextual menu with a list of callers.
+You can also use the Back button (left arrow) in the toolbar.
+The Information panel also offers navigation possibilities between
+variables and their definitions.
+
+In the graphical interface, three panels (displayed below the
+source code) are very useful for \Eva{}: Properties, Values, and
+Red Alarms. Further details about the GUI are presented in chapter~\ref{gui}.
+For now, it suffices to say that:
+
+\begin{itemize}
+\item Properties displays (among others) the list of alarms in the program;
+\item Values displays the inferred values for the expression selected in the
+ Frama-C normalized source code (highlighted in green);
+\item Red Alarms displays some special cases of alarms that should be considered
+ first.
+\end{itemize}
+
+In the GUI, each alarm is represented with a ``bullet'' to its left.
+Red bullets mean ``this {\em always} happens''; yellow
+bullets mean ``this {\em may} happen (but I am not sure, due to
+approximations)''. When there are several alarms, some strategies allow
+prioritizing which alarms are more likely to correspond to actual issues.
+
+The overall rule of thumb when inspecting alarms in the GUI\footnote{The first
+ time the Frama-C GUI is run, the Properties panel displays several kinds of
+ properties. For \Eva{}, the most useful view consists in selecting the
+ ``Reset 'Status' filters to show only unproved/invalid'' option, using the
+ button next to ``Refresh'' in the Properties panel.} is the following:
+
+\begin{itemize}
+\item inspect red alarms in the Properties panel; these correspond to
+ situations where the analysis is {\em certain} that a problem has arrived;
+ either an actual bug in the code, or some issue in the analysis that needs to
+ be addressed (e.g. due to missing or incorrect specifications);
+\item inspect the cases present in the Red Alarms panel; these are situations
+ which are likely to correspond to definitive problems, and thus should be
+ treated before others\footnote{The {\em exact} meaning of such red alarms is
+ too complex to be presented here; as a first approximation, these can be
+ seen as intermediate between red and yellow alarms.};
+\item inspect remaining cases (yellow alarms) in the Properties panel.
+\end{itemize}
+
+In the case of our remaining alarm, it is yellow, but it appears in the
+Red Alarms panel. This indicates it is more likely to correspond to a real
+issue.
+
+Extra information can be observed by clicking the alarm in the Red Alarms tab,
+which highlights it in the source code, then selecting expression
+\lstinline|hash| in line 17 and reading the \textsf{Values} tab:
\begin{logs}
[0] $\in$ {200}
[1..7] $\in$ UNINITIALIZED
@@ -837,54 +835,16 @@ This means that element \lstinline|hash[0]| has value 200, but elements 1 to 7
are definitely uninitialized. Therefore the first iteration of the loop
proceeds as expected, but on the second iteration, the analysis of the branch
is stopped, because
-from the point of view of the analyzer reading an uninitialized
+from the point of view of the analyzer, reading an uninitialized
value should be a fatal error. And there are no other execution
branches that reach the end of this loop, which is why the analyzer
-finds that function \lstinline|main| does not terminate.
-
-The next warning, \lstinline|accessing uninitialized left-value...|
-is emitted whenever an accessed value may be uninitialized, and the emitted
-assertion, \lstinline|\initialized(&hash[i])|, could not be verified by
-\Eva{}, and must therefore be verified by other means
-(eventually, other Frama-C analyses) to ensure the behavior of the code is
-defined.
-
-\subsection{Making sense of alarms}
-
-There were three alarms in the analysis. The other two are related to
-interactions between
-the Frama-C standard library and our own implementations of \verb|memset|/
-\verb|memcpy|\footnote{Namely, the fact that their specifications involve
-{\em logic predicates} that are not yet understood by \Eva{} leads
-to an ``Unknown'' status, even though they are valid in this case.},
-but we can safely ignore them here.
-
-
-%% There are three alarms in the analysis we now have, and two of them are related
-%% to the (lack of) \lstinline|printf| specification, because we did not include
-%% that of the Frama-C standard library. Because \lstinline|printf| does not
-%% modify the values of any variables we are interested in, and we do not want to
-%% provide it with some code, we can simply add a minimalistic ACSL specification
-%% to the \lstinline|printf| prototype in line 3:
-
-%% \begin{listing}{3}
-%% /*@ assigns \result \from \nothing; */
-%% int printf(const char*,...);
-%% \end{listing}
-
-%% This is incorrect in the general case (since it claims that the result of
-%% \lstinline|printf| is a constant value, independent of its arguments),
-%% but since we ignore its result in our code anyway, this is fine here.
-%% This is by the way equivalent to the default behavior that was previously
-%% inferred by \Eva{}, and the reason why it emitted warnings:
-%% it is not a correct specification in the general case.
-
-Furthermore, the program
-is also found not to terminate. This means that every execution
-either encounters the problem from line 14 in \lstinline|main_1.c|,
-or an infinite loop somewhere else in the program.
-We should, therefore, pay particular attention to this alarm.
+finds that function \lstinline|main| does not terminate (the log contains
+the message ``NON TERMINATING FUNCTION'').
+\subsection{Finding and fixing bugs}
+
+We found a real issue in the code, but to find the exact cause it is necessary
+to investigate the code.
Looking again at the header file \lstinline|skein.h|, we may now
notice that in function \lstinline|Skein_256_Init|,
the formal parameter for the desired hash length is named
@@ -892,19 +852,13 @@ the formal parameter for the desired hash length is named
We were inadvertently asking for a 1-char hash of the message
since the beginning, and the test that we ran as our first
step failed to notice it.
-Our first imprecise analysis did find it -- the same alarm that
-pointed out the problem is present among the other alarms produced
-by the first analysis. Note that because of the imprecisions,
-the first analysis was not able to conclude that the uninitialized access
-at \lstinline|hash[2]| was certain, making it much less noticeable
-among the others.
The bug can be fixed by passing
8*HASHLEN instead of HASHLEN as the second argument of
\lstinline|Skein_256_Init|.
With this fix in place, the analysis
-with \lstinline|-eva-slevel 100| produces no alarms (apart from the postconditions
-of \verb+memcpy+ and \verb+memset+) and gives the following result:
+with \lstinline|-eva-precision 3| produces no alarms and gives the following
+result:
\begin{logs}
Values for function main:
hash[0] $\in$ {40}
@@ -968,7 +922,7 @@ defines \lstinline|Frama_C_interval|. Running Frama-C on this
file (without \verb|main_1.c| in the same directory, to avoid having two
definitions for \verb|main|):
\begin{shell}
-frama-c -eva-slevel 100 -eva *.c >log 2>&1
+frama-c -eva-precision 3 -eva *.c >log 2>&1
\end{shell}
This time, the absence of actual alarms is starting to be really interesting:
@@ -1055,7 +1009,7 @@ sequence, let us now compute the functional dependencies of each function.
Functional dependencies list, for each output location,
the input locations that influence the final contents of this output location:
\begin{shell}
-frama-c -eva *.c -eva-slevel 100 -deps
+frama-c -eva *.c -eva-precision 3 -deps
\end{shell}
\begin{logs}
Function Skein_256_Init:
@@ -1063,7 +1017,7 @@ Function Skein_256_Init:
.h{.bCnt; .T[0..1]; } FROM ctx
.X[0..3] FROM msg[0..63];
skein_context{.X[0..3]; .b[0..31]; }; ctx;
- hashBitLen; ONE[bits 0 to 7] (and SELF)
+ hashBitLen; Skein_Swap64_ONE[bits 0 to 7] (and SELF)
.b[0..31] FROM ctx (and SELF)
\result FROM \nothing
@@ -1080,12 +1034,12 @@ Function Skein_256_Update:
Function Skein_256_Final:
hash[0..7] FROM msg[0..79]; skein_context; ctx;
- hashVal; ONE[bits 0 to 7] (and SELF)
+ hashVal; Skein_Swap64_ONE[bits 0 to 7] (and SELF)
skein_context.h.bCnt FROM skein_context.h.hashBitLen; ctx (and SELF)
.h.T[0] FROM skein_context.h{.hashBitLen; .bCnt; .T[0]; }; ctx
.h.T[1] FROM skein_context{.h.hashBitLen; .h.T[1]; }; ctx
{.X[0..3]; .b[0..15]; } FROM msg[0..79]; skein_context;
- ctx; ONE[bits 0 to 7] (and SELF)
+ ctx; Skein_Swap64_ONE[bits 0 to 7] (and SELF)
.b[16..31] FROM skein_context.h.bCnt; ctx (and SELF)
\result FROM \nothing
\end{logs}
@@ -1112,20 +1066,20 @@ dependencies are normal or reveal a problem. Let us move on to the
functional dependencies of \lstinline|do_Skein_256|:
\begin{logs}
Function do_Skein_256:
- hash[0..7] FROM msg[0..79]; ONE[bits 0 to 7] (and SELF)
+ hash[0..7] FROM msg[0..79]; Skein_Swap64_ONE[bits 0 to 7] (and SELF)
\end{logs}
These dependencies make the effect of the functions clearer. The
\verb|FROM msg[0..79]| part is what we expect. The
\verb|and SELF| mention is an unfortunate approximation. The
-dependency on global variable \verb|ONE| reveals an implementation
+dependency on global variable \verb|Skein_Swap64_ONE| reveals an implementation
detail of the library (the variable is used to detect endianness
dynamically). Finding out about this variable is a good thing: it
shows that a possibility for a malicious programmer to corrupt the
implementation into hashing the same message to different digests
-would be to try to change the value of \verb|ONE| between
+would be to try to change the value of \verb|Skein_Swap64_ONE| between
computations. Checking the source code for mentions of variable
-\lstinline|ONE|, we can see it is used to
+\lstinline|Skein_Swap64_ONE|, we can see it is used to
detect endianness and is declared \lstinline|const|. On an
MMU-equipped platform, there is little risk that this variable
could be modified maliciously from the outside.
@@ -1133,7 +1087,7 @@ However, this is a vivid example of how static
analysis, and especially correct analyses as provided in Frama-C, can
complement code reviews in improving trust in existing C code.
-Assuming that variable \lstinline|ONE| keeps its value, a same
+Assuming that variable \lstinline|Skein_Swap64_ONE| keeps its value, a same
input message is guaranteed always to be hashed by this
sequence of calls to the same digest,
because option \verb|-deps| says that there is no other
@@ -1164,8 +1118,10 @@ The latter condition is harder than the former.
Observing results (with the GUI or observation functions
described in section \ref{buitins_observation}) can help to iterate towards
a solution. Be creative. The continuation of this tutorial can be found online
-at \url{http://blog.frama-c.com/index.php?tag/skein}; read
-available posts in chronological order.
+at \url{http://blog.frama-c.com/index.php?tag/skein}\footnote{Note that some
+ messages and options have changed since the tutorial was posted. Using an
+ older Frama-C version may be necessary to obtain similar results.}
+; read available posts in chronological order.
% This tutorial is TO BE CONTINUED.\\
% ~\\
@@ -1548,7 +1504,7 @@ enable such alarms.
\listinginput{1}{lshift.c}
\begin{logs}
-lshift.c:4:[kernel] warning: invalid LHS operand for left shift. assert 0 <= x;
+[eva:alarm] lshift.c:4: Warning: invalid LHS operand for left shift. assert 0 <= x;
\end{logs}
\subsubsection{Overflow in integer arithmetic}
@@ -1562,28 +1518,23 @@ paragraph 6.5.5 of the ISO/IEC 9899:1999 standard.
If useful, it is also possible to assume that signed integers overflow
according to a 2's complement representation. The option
\lstinline|-no-warn-signed-overflow| can be used to this end. A
-reminder message is nevertheless emitted operations that are detected
-as potentially overflowing.
-%
-Regardless of the value of option \lstinline|-warn-signed-overflow|,
-a warning is emitted on signed arithmetic
-operations applied to the cast to signed int of an address, since the
-compiler may place variables in memory at will.
+reminder warning is nevertheless emitted on operations that are detected
+as potentially overflowing. This warning can also be disabled by option
+\lstinline|-eva-warn-key signed-overflow=inactive|.
By default, no alarm is emitted for arithmetic operations on unsigned integers
for which an overflow may happen, since such operations have
defined semantics according to the ISO/IEC 9899:1999 standard.
-If one wishes to signal and prevent such unsigned overflows,
+If one wishes to signal and prevent such unsigned overflows,
option \verb+-warn-unsigned-overflow+ can be used.
-Finally, no alarm is emitted for downcasts to signed or unsigned
-integers. In the signed case, the least significant bits
+Finally, by default, no alarm is emitted for downcasts to signed or unsigned
+integers. In the signed case, the least significant bits
of the original value are used, and are interpreted according
to 2's complement representation.
Frama-C's options \lstinline|-warn-signed-downcast| and
-\lstinline|-warn-unsigned-downcast| are not honored by \Eva{}.
-The RTE plug-in can be used to generate the relevant assertions
-before starting an analysis.
+\lstinline|-warn-unsigned-downcast| can be used to emit alarms on signed
+or unsigned downcasts that may exceed the destination range.
\subsubsection{Overflow in conversion from floating-point to integer}
@@ -1593,8 +1544,8 @@ range of the integer type it is converted to.
\listinginput{1}{ov_float_int.c}
\begin{logs}
...
-ov_float_int.c:6:[kernel] warning: overflow in conversion from floating-point
- to integer. assert -2147483649 < f < 2147483648;
+[eva:alarm] ov_float_int.c:6: Warning: overflow in conversion from floating-point
+ to integer. assert f < 2147483648;
[eva] Values at end of function main:
f $\in$ [2000000000. .. 3000000000.]
@@ -1614,7 +1565,7 @@ first kind of alarm can be seen in the following example.
frama-c -eva -main sum double_op_res.c
\end{shell}
\begin{logs}
-double_op_res.c:3:[kernel] warning: non-finite double value
+[eva:alarm] double_op_res.c:3: Warning: non-finite double value.
assert \is_finite((double)(a+b));
\end{logs}
@@ -1632,7 +1583,7 @@ See the example below.
frama-c -eva double_op_arg.c
\end{shell}
\begin{logs}
-double_op_arg.c:7:[kernel] warning: non-finite float value:
+[eva:alarm] double_op_arg.c:7: Warning: non-finite float value.
assert \is_finite(bits.f);
\end{logs}
@@ -1785,7 +1736,7 @@ parsing. Each of these only mean that an expression with side-effects
will require checking after the Abstract Syntax Tree has been elaborated.
For instance, the first of these warnings is:
\begin{logs}
-se.c:5:[kernel] warning: Unspecified sequence with side effect:
+[kernel] se.c:5: Warning: Unspecified sequence with side effect:
/* <- */
tmp = x;
/* x <- */
@@ -1797,8 +1748,10 @@ se.c:5:[kernel] warning: Unspecified sequence with side effect:
Then \Eva{} is run on the program.
In the example at hand, the analysis finds problems at lines 5 and 7.
\begin{logs}
-se.c:5: ... undefined multiple accesses in expression. assert \separated(&x, &x);
-se.c:7: ... undefined multiple accesses in expression. assert \separated(&x, p);
+[eva:alarm] se.c:5: Warning: undefined multiple accesses in expression.
+ assert \separated(&x, &x);
+[eva:alarm] se.c:7: Warning: undefined multiple accesses in expression.
+ assert \separated(&x, p);
\end{logs}
At line 5, it can guarantee that an undefined behavior exists, and the analysis
is halted.
@@ -1830,7 +1783,7 @@ Vaguely related to, but different from, undefined side-effects in expressions,
\listinginput{1}{overlap.c}
-The programmer thought ey was invoking implementation-defined behavior
+The programmer thought implementation-defined behavior was invoked
in the above program, using an union to type-pun between structs S and T.
Unfortunately, this program returns 1 when compiled
with \lstinline|clang -m32|; it returns 2 when compiled
@@ -1882,7 +1835,8 @@ and \lstinline|int *| are \emph{not} compatible).
[eva:alarm] valid_function.c:9: Warning:
pointer to function with incompatible type. assert \valid_function(p);
[kernel:annot:missing-spec] valid_function.c:9: Warning:
- Neither code nor specification for function f1, generating default assigns from the prototype
+ Neither code nor specification for function f1, generating default assigns
+ from the prototype
[eva] using specification for function f1
[eva:alarm] valid_function.c:12: Warning:
pointer to function with incompatible type. assert \valid_function(p);
@@ -1927,7 +1881,7 @@ they do {\bf not} use the word ``assert''.
These messages
are intended to help the user trace the results of the analysis, and
give as much information as possible in order to help
-em find when and why the analysis becomes imprecise.
+them find when and why the analysis becomes imprecise.
These messages are only useful when it is important to analyze the application
with precision. \Eva{} remains correct even when it
is imprecise.
@@ -1936,21 +1890,75 @@ is imprecise.
Examples of messages that result from the apparition of imprecision in the
analysis are:
\begin{logs}
-origin.c:14:[eva] assigning imprecise value to pa1.
- The imprecision originates from Arithmetic {origin.c:14}
+[eva] origin.c:14:
+ Assigning imprecise value to pa1.
+ The imprecision originates from Arithmetic {origin.c:14}
-origin.c:15:[eva] writing somewhere in {ta1}
- because of Arithmetic {origin.c:14}.
+[eva] origin.c:15:
+ writing somewhere in {ta1} because of Arithmetic {origin.c:14}.
\end{logs}
Examples of messages that correspond to unusual circumstances are:
\begin{logs}
-alloc.c:20: ... all target addresses were invalid.
- This path is assumed to be dead.
+[kernel] alloc.c:20: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
-origin.i:86: ... local escaping the scope of local_escape_1 through esc2
+[eva:locals-escaping] origin.i:86: Warning:
+ locals {x} escaping the scope of local_escape_1 through esc2
\end{logs}
+Note that a few messages are prefixed with \verb|[kernel]| instead of
+\verb|[eva]|, for technical reasons, but it is the analysis by \Eva{}
+which causes them to be emitted.
+
+\subsection{Analysis summary}
+
+At the end of the analysis, \Eva{} produces a summary such as the
+following:
+
+\begin{logs}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 6 functions analyzed (out of 44): 13% coverage.
+ In these functions, 588 statements reached (out of 626): 93% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 143 alarms generated by the analysis:
+ 71 integer overflows
+ 64 accesses to uninitialized left-values
+ 8 illegal conversions from floating-point to integer
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 11 valid 0 unknown 0 invalid 11 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
+\end{logs}
+
+It contains:
+
+\begin{itemize}
+\item semantic coverage metrics, with the number of functions and
+ statements analyzed;
+\item total number of errors and warnings, pointing out potential issues that
+ could jeopardize the correction of the analysis;
+\item total number of alarms emitted by the analysis, grouped by kind;
+\item total number of logical properties (assertions and preconditions at each call-site)
+ proven by the analysis.
+ Note that this only indicates the logical statuses evaluated by \Eva{};
+ some logical properties may have been proven by other plugins.
+\end{itemize}
+
+The summary provides a quick glance at the analysis, being especially useful
+for side-by-side comparisons of different parametrizations. It also allows
+one to quickly determine whether there remain issues to be resolved.
+More detailed information is provided through the graphical interface and
+by the Report plugin.
+
+The summary display can be disabled by using option
+\lstinline|-eva-msg-key=-summary|.
+
\section{About these alarms the user is supposed to check\ldots}
@@ -1959,9 +1967,9 @@ reverse-engineering source code, it does not really make sense to expect
the user to check the alarms that are emitted by \Eva{}.
Consider for instance Frama-C's slicing plug-in. This plug-in produces
a simplified version of a program. It is often applied to large unfamiliar
-codebases; if the user is at the point where ey needs a slicer to make
+codebases; if the user is at the point where they need a slicer to make
sense of the codebase, it's probably a bad time to require
-em to check alarms on the original unsliced version.
+them to check alarms on the original unsliced version.
The slicer and other code comprehension plug-ins work around this problem
by defining the results they provide as ``valid for well-defined executions''.
@@ -2182,7 +2190,7 @@ is as precise as the result obtained for the example in section \ref{boucles}.
\listinginput{1}{fonctions.c}
-Calls to variadic functions are handled by the {\em Variadic} plug-in, which
+Calls to variadic functions are handled by the \textsf{Variadic} plug-in, which
translates calls to variadic functions into semantically-equivalent calls,
either using arrays as arguments or via calls to specialized variants of the
function. Such translations are enabled by default whenever the corresponding
@@ -2389,7 +2397,7 @@ For each C language construct that is not completely specified by the
standard, there may exist an alternative, ``portable''
version. The portable version could be considered safer if the
programmer did not know exactly how the non-portable version will be
-translated by eir compiler. But the portable version may
+translated by their compiler. But the portable version may
produce a code which is significantly slower and/or bigger. In practice,
the constraints imposed on embedded software often lead to choosing
the non-portable version. This is why, as often as possible, \Eva{}
@@ -2457,18 +2465,18 @@ respect to the same base address.
The strongest hypothesis that the plug-in relies on is about the representation
of memory and can be expressed in this way:
-{\bf It is possible to pass from one address to another through the addition
+{\bf it is possible to pass from one address to another through the addition
of an offset, if and only if the two addresses share the same base address}.
\medskip
-This hypothesis is not true in the C language itself : addresses
+This hypothesis is not true in the C language itself: addresses
are represented with a finite number of bits, 32 for instance,
-and it is always possible to compute an offset to go from on address
+and it is always possible to compute an offset to go from an address
to a second one by considering them as integers and subtracting the
first one from the second one.
The plug-in generates all the alarms that ensure, if they are checked,
that the analyzed code fits in this hypothesis. On the following example,
-it generates a proof obligation that means that ``the comparison
+it generates a proof obligation meaning that ``the comparison
on line 8 is safe only if \lstinline|p| is a valid address or if the base address
of \lstinline|p| is the same as that of \lstinline|&x|''.
\listinginput{1}{bases.c}
@@ -2520,7 +2528,7 @@ Dynamic allocation is modeled by creating new bases.
Each call to \lstinline|malloc| and \lstinline|realloc| potentially creates a
new base, depending on the \emph{builtins} (described in section~\ref{libc})
used -- possibly resulting in an unbounded number of such bases.
-Dynamically allocated bases behave mostly like statically allocated one,
+Dynamically allocated bases behave mostly like statically allocated ones,
except that they come in two flavors:
%
\begin{itemize}
@@ -2644,40 +2652,60 @@ 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{three-step} presents the overall methodology recommended when
+using \Eva{}, especially for realistic code bases.
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
+tuning options. Section \ref{nonterm} presents a derived analysis to
obtain information about non-termination.
+Finally, section \ref{analysis-scripts} presents some scripts and templates
+to help bootstrap an analysis and automate some of its steps.
+
+\section{Three-step approach}
+\label{three-step}
+
+For realistic code bases, an analysis with \Eva{} requires several steps which
+are better performed separately, for several reasons:
+
+\begin{itemize}
+\item errors are confined to each of the separate steps, instead of being
+ mingled together;
+\item partial results can be saved and reused, avoiding unnecessary
+ recomputations;
+\item it is clearer which options and changes affect which stages, leading to
+ better understanding of the process.
+\end{itemize}
+
+The recommended approach can be summarized as follows:
+
+\begin{itemize}
+\item parsing sources: \verb|frama-c <sources> -save parsed.sav|;
+\item running \Eva{}: \verb|frama-c -load parsed.sav -eva -save eva.sav|;
+\item viewing its results on the GUI: \verb|frama-c-gui -load eva.sav|.
+\end{itemize}
+
+The commands and options are detailed in the next section.
\section{Command line}
\label{command-line}
The parameters that determine Frama-C's behavior can be
-set through the command line.
-The command to use to launch the tool is:
-\begin{shell}
-frama-c-gui <options> <files>
-\end{shell}
-Most parameters can also be set after the tool is launched,
-in the graphical interface.
-
+set through the command line. There are two main variants of Frama-C,
+one based on the command line (\lstinline|frama-c|), and one which launches
+a graphical interface (\lstinline|frama-c-gui|).
The options understood by the \Eva{} plug-in are described in
-this chapter. The files are the C files containing source code
-to analyze.
-
-For advanced users and plug-in developers, there exists
-a ``batch'' version of Frama-C. The executable for the batch version is named
-\lstinline|frama-c| (or \lstinline|frama-c.exe|). All options of \Eva{}
-work identically for the GUI and batch version of Frama-C.
+this chapter.
+All options of \Eva{} work identically for both the graphical interface
+and for the command line.
\bigskip
The options documented in this manual can be listed,
-with short descriptions, from the command-line.
+with short descriptions, from the command line.
Option \lstinline|-kernel-help|
lists options that affect all plug-ins. Option
\lstinline|-eva-help| lists options specific to the
@@ -2697,10 +2725,12 @@ $\dots$
$\dots$
\end{logs}
-\textbf{Note:} historically, \Eva{} was called Value, and most of its options
-were prefixed with \lstinline|-val|. All \lstinline|-val-*| options
-are aliased to equivalent \lstinline|-eva-*| functions; negative options of
-the form \lstinline|-no-val-*| are aliased to \lstinline|-eva-no-*|.
+\begin{important}
+ Historically, \Eva{} was called Value, and most of its options
+ were prefixed with \lstinline|-val|. All \lstinline|-val-*| options
+ are aliased to equivalent \lstinline|-eva-*| functions; negative options of
+ the form \lstinline|-no-val-*| are aliased to \lstinline|-eva-no-*|.
+\end{important}
\subsection{Analyzed files and preprocessing}\label{sec:analyz-files-prepr}
@@ -2715,7 +2745,12 @@ to which the option \lstinline|-x c| should be passed in order to pre-process
C files that do not have a \lstinline|.c| extension.
\goodbreak
-The option \lstinline|-cpp-command <cmd>| sets the preprocessing command to use.
+Option \lstinline|-cpp-extra-args <options>| allows giving additional options
+to the preprocessor, usually \verb|-D| for defining macros and \verb|-I| for
+including header directories.
+
+In rare cases, you may need to use a different preprocessing command, via
+option \lstinline|-cpp-command <cmd>|.
If the patterns \lstinline|%1| and \lstinline|%2| do not appear
in the text of the
command, Frama-C invokes the preprocessor in the following way:
@@ -2723,7 +2758,6 @@ command, Frama-C invokes the preprocessor in the following way:
<cmd> -o <outputfile> <inputfile>
\end{shell}
-
In the cases where it is not possible to invoke the preprocessor with
this syntax, it is possible to use the
patterns \lstinline|%1| and \lstinline|%2|
@@ -2763,10 +2797,22 @@ back into memory for visualization or further computations.
Example :
\begin{shell}
-frama-c -eva -deps -out -save result file1.c file2.c
-frama-c-gui -load result
+frama-c -eva -deps -out -save result.sav file1.c file2.c
+frama-c-gui -load result.sav
\end{shell}
+\begin{important}
+ There is no specific extension for Frama-C saved files; the usual
+ convention is to use \verb|.sav|.
+\end{important}
+
+\begin{important}
+ Most options are saved when \verb|-save| is used and do not need to
+ be passed again when loading it. It is therefore useful to separate
+ parsing options from analysis options, the former to be saved after
+ parsing, the latter to be given after loading it.
+\end{important}
+
\subsection{Controlling the output}
By default, \Eva{} emits all the alarms it finds (section
@@ -2846,7 +2892,7 @@ you should make use of the non-deterministic primitives described in
section \ref{nondeterminism} to write an alternative entry point
for the analysis like this:
\begin{listing-nonumber}
-int analysis_main(void)
+int eva_main(void)
{
char *argv[3];
char arg[2];
@@ -2862,7 +2908,7 @@ int analysis_main(void)
For this particular example, the initial state that was
automatically generated includes the desired one. This may however
not always be the case. Even when it is the case, it is desirable
-write an analysis entry point that positions the
+to write an analysis entry point that positions the
values of \lstinline|argc| and \lstinline|argv| to
improve the relevance of the alarms emitted by \Eva{}.
@@ -3090,6 +3136,8 @@ compiled with the same compiler as the one intended to compile the
analyzed application. If this is not possible, the analysis can also be
parameterized manually with the characteristics of the target
architecture.
+The Frama-C Plugin Development Guide~\cite{plugin-dev-guide} contains a
+section about customizing the machine model.
\subsection{Parameterizing the modeling of the C language}
@@ -3241,6 +3289,7 @@ that enable the analyzer to maintain precision while ensuring the analysis
time remains bounded.
\subsection{Loop unrolling}
+\label{loop-unroll}
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.
@@ -3288,9 +3337,8 @@ 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-unroll| to be informed whenever the specified
-unrolling value is insufficient to unroll the loop entirely:
+objective is full unrolling; for this reason, the user is informed whenever
+the specified unrolling value is insufficient to unroll the loop entirely:
\begin{lstlisting}
void main() {
@@ -3304,6 +3352,8 @@ void main() {
[eva:loop-unroll] insuf-loop.c:3: loop not completely unrolled
\end{lstlisting}
+The message can be deactived via \lstinline|-eva-warn-key loop-unroll=inactive|.
+
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.
@@ -3378,7 +3428,10 @@ the analyzed application. The \lstinline|-eva-slevel-function| option can be use
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,
+However, it is in many cases superseded by \lstinline|-eva-precision|, which
+controls other parameters related to analysis precision and speed.
+Also, \lstinline|-eva-slevel| 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.
@@ -3479,8 +3532,10 @@ be applied to them.
\subsubsection*{Deprecated: \texttt{WIDEN\_HINTS} loop pragma}
-\textbf{Note:} this syntax has been deprecated in favor of the previous one
-and it is kept here only for reference.
+\begin{important}
+ This syntax has been deprecated in favor of the previous one
+ and it is kept here only for reference.
+\end{important}
The \lstinline|loop widen_hints| annotation above has an obsoleted syntax: \\
\lstinline|//@ loop pragma WIDEN_HINTS $v_1,\ldots,v_n$, $e_1,\ldots,e_m$ ;|\\
@@ -3985,19 +4040,19 @@ during the initial part of an analysis, they may blend in with the sets
of possibly false alarms. However, priority should be given to these
alarms, since they are likely to indicate an incorrect parameterization.
-To help identify these situations, the {\em Nonterm} plug-in has been
+To help identify these situations, the \textsf{Nonterm} plug-in has been
developed. It runs after \Eva{}, by adding \verb|-then -nonterm|
at the end of the command-line.
-{\em Nonterm} emits warnings about non-terminating instructions in functions
+\textsf{Nonterm} emits warnings about non-terminating instructions in functions
analyzed by \Eva{}. It operates on a per-callstack basis, and therefore
displays more precise results than a visual inspection on the GUI;
in particular, if there are both terminating and non-terminating callstacks for
a given statement, the GUI will not color their successors red
-(because of the terminating callstacks), but {\em Nonterm} will emit warnings
+(because of the terminating callstacks), but \textsf{Nonterm} will emit warnings
for the non-terminating ones.
-{\em Nonterm} only reports situations where \Eva{} is able to
+\textsf{Nonterm} only reports situations where \Eva{} is able to
guarantee non-termination. Because its purpose is to prioritize warnings
that are likely to indicate parameterization errors,
it does not consider callstacks where termination seems possible.
@@ -4014,6 +4069,34 @@ amount of warnings and is rarely needed in practice.
% TODO: plevel, wlevel?
+\section{Analysis scripts and templates}\label{analysis-scripts}
+
+Setting up an analysis is a process that takes some time. Iterating an
+analysis (changing the parametrization, adding annotations, etc.) is a process
+which can greatly benefit from a structured approach, for instance to avoid
+reparsing the sources when only \Eva{}-related options are modified.
+For both tasks, Frama-C offers some templates and scripts to help the user.
+
+The files themselves are located mostly in Frama-C's \verb|share| directory
+(\verb|FRAMAC_SHARE|, when running \verb|frama-c-config|), but they can be
+accessed via the \verb|frama-c-script| command, among which we cite:
+
+\begin{description}
+\item[make-template]: creates a Makefile template in the current directory.
+ This template follows the recommended three-step setup
+ (section~\ref{three-step}), tracks dependencies (e.g. re-running parsing
+ when source files are modified) and offers useful targets for the user.
+\item[find-fun]: useful to find which source files declare/define a given
+ function; for instance, when there are multiple \verb|main| functions.
+\item[flamegraph]: opens a {\em flamegraph}\footnote{See
+ https://github.com/brendangregg/FlameGraph for details about flamegraphs.}
+ (a graphical profiling tool) of the analysis performed by \Eva{}.
+\end{description}
+
+Running \verb|frama-c-script| without arguments outputs the list of
+currently-available commands\footnote{The list of commands is liable to change
+ for each Frama-C release.}.
+
\chapter{Inputs, outputs and dependencies}\label{inoutdeps}
\vspace{2cm}
@@ -4782,9 +4865,8 @@ form:
\end{listing-nonumber}
This indicates that new bases are being created.
-The analysis will then have to be manually interrupted.
-You will then need to either entirely unroll the loop ({\it e.g.} giving
-the analysis enough \lstinline|slevel|), or use a weak variant.
+You must then manually interrupt the analysis and either unroll the loop
+entirely (see Section~\ref{loop-unroll}) or use a weak variant.
By default, \emph{weak} builtins are used, but usage of
\lstinline|-eva-builtin| takes precedence over preexisting associations.
@@ -5019,7 +5101,10 @@ Builtins for functions of the \lstinline|string.h| standard header.
\lstinline|Frama_C_strnlen|
\end{tabular}
\end{table}
-Note: \lstinline|rawmemchr| is a GNU extension to standard C.
+
+\begin{important}
+ \lstinline|rawmemchr| is a GNU extension to standard C.
+\end{important}
\ifdefstring{\OPENSOURCE}{no}{
% These builtins are not available in the open-source release
@@ -5213,33 +5298,31 @@ return \lstinline|6| and \lstinline|36| respectively.
\newcommand{\question}[1]{\stepcounter{question}{\vspace{5mm}\noindent \bf {\large Q.\arabic{question}}~~~{#1}\medskip}}
\question{Which option should I use to improve the handling of loops
- in my program, {\tt -ulevel} or {\tt -eva-slevel}?}
-
-The options \lstinline|-ulevel| and \lstinline|-eva-slevel| have different sets of
-advantages and drawbacks. The main drawback of \lstinline|-ulevel| is that
-it performs a syntactic modification of the analyzed source code,
-which may hamper its manipulation. On the other hand, syntactic
-unrolling, by explicitly separating iteration steps, allows to use
-the graphical user interface
-\lstinline|frama-c-gui| to observe values or express properties for a
-specific iteration step of the loop.
-
-The \lstinline|-eva-slevel| option does not allow to observe a specific
-iteration step of the loop. In fact, this option may even be a little
-confusing for the user when the program contains loops for which the
-analysis cannot decide easily the truth value of the condition,
-nested loops, or if-then-else
-statements\footnote{if-then-else statements are ``unrolled''
- in a manner similar to loops}. The main advantages of this option are
-that it leaves the source code unchanged and that it works with
-loops that are built using \lstinline|goto|s instead of \lstinline|for| or \lstinline|while|.
-% The \lstinline|-eva-slevel| option requires less memory than
-% \lstinline|-ulevel|, and as a consequence it can sometimes be faster.
-It also improves precision when evaluating \lstinline|if| or
-\lstinline|switch| conditionals.
-A current drawback of semantic unrolling is that it can only be specified
-crudely at the function level, whereas syntactic unrolling can be
-specified loop by loop.
+ in my program?}
+
+The recommended way is to use \lstinline|loop unroll| annotations on a case by
+case basis, which is the most precise and stable mechanism currently in \Eva{}.
+Alternatively, using \lstinline|-eva-slevel| is the next best approach.
+This option is more costly, often hard to predict, and can only be specified
+globally or at the function level (via \lstinline|-eva-slevel-function|).
+However, it works for loops that are built using \lstinline|goto|s instead of
+\lstinline|for| or \lstinline|while|, and it also improves precision when
+evaluating \lstinline|if| or \lstinline|switch| conditionals (but it is consumed
+by them, which can be confusing for the user).
+
+Both approaches do have a minor drawback, in that they do not allow to observe
+a specific iteration step of the loop. The main advantage of these options is
+that they leave the source code unchanged.
+
+The Frama-C kernel has an option \lstinline|-ulevel|, which performs a
+syntactic modification of the analyzed source code. Its advantage is that,
+by explicitly separating iteration steps, it allows to use
+the graphical user interface to observe values or express properties for a
+specific iteration step of the loop. However, the duplication of loop
+statements and variables can lead to cluttered code. Also, the transformation
+increases the size of the code in the Frama-C AST and, for large functions,
+this has a significant impact in the analysis
+time. For these reasons, \lstinline|-ulevel| is seldom used nowadays.
\question{Alarms that occur after a true alarm in the analyzed code
@@ -5261,7 +5344,7 @@ perform a choice over what may happen after dereferencing
\lstinline|NULL|. It is possible to give some new information to the tool
so that analysis can continue after a true alarm. This technique is called
debugging. Once the issue has been corrected in the source code under
-analysis ---~more precisely, once the user has convinced emself
+analysis ---~more precisely, once the user has convinced themselves
that there is no problem at this point in the source code~--- it
becomes possible to trust the alarms that occur after the given point,
or the absence thereof (see next question).
@@ -5285,9 +5368,8 @@ happens in the following example:
Analyzing this example with the default options produces:
\begin{logs}
-false_al.c:7:[kernel] warning: accessing out of bounds index [-100..100].
- assert 0 <= i < 101;
-false_al.c:9:[kernel] warning: division by zero: assert y != 0;
+[eva:alarm] false_al.c:7: Warning: accessing out of bounds index. assert 0 <= i;
+[eva:alarm] false_al.c:9: Warning: division by zero. assert y != 0;
\end{logs}
On line 7, the tool is only capable of detecting that \lstinline|i| lies in
@@ -5298,74 +5380,76 @@ proceeds with the analysis, the plug-in detects that line 8 is safe, and
that there is an alarm on line 9. These results must be interpreted
thus: assuming that the array access on line 7 was legitimate, then
line 8 is safe, and there is a threat on line 9. As a consequence, if
-the user can convince emself that the threat on line 7 is false,
-ey can trust these results ({\it i.e.} there is nothing to worry
+the user can convince themselves that the threat on line 7 is false,
+they can trust these results ({\it i.e.} there is nothing to worry
about on line 8, but line 9 needs further investigation).
%\bigskip
%\bigskip
-\question{In my annotations, macros are not pre-processed. What should
- I do?}
-
-The annotations being contained inside C comments, they
-{\it a priori} aren't affected by the preprocessing. It is possible
-to instruct Frama-C to launch the preprocessing on annotations
-with the option \lstinline|-pp-annot| (activated by default). Note that this option requires the
-preprocessor to be GNU \lstinline|cpp|, the GCC preprocessor\footnote{More
- precisely, the preprocessor must understand the {\tt -dD} and the
- {\tt -P} options that outputs macros definitions along with the
- pre-processed code and inhibits the generation of {\tt \#line}
- directives respectively.}.
-
-A typical example is as follows.
-\listinginputcaption{1}{\texttt{array.c}}{array.c}
-It is useful to use the pre-processor constant \lstinline|N|
-in the post-condition of function \lstinline|get_index()|.
-Use the command-line:
-\begin{shell}
-frama-c -eva array.c -pp-annot
-\end{shell}
-\medskip
-
-Note that when using this option, the preprocessing is
-made in two passes (the first
-pass operating on the code only, and the second operating on the
-annotations only). For this reason, the options passed to
-\lstinline|-cpp-command| in this case should only be commands that can
-be applied several times without ill side-effects. For instance,
-the \lstinline+-include+ option to \lstinline|cpp| is a command-line equivalent
-of the \lstinline+#include+ directive. If it was passed to \lstinline+cpp-command+
-while the preprocessing of annotations is being used, the
-corresponding header file would be included twice. The Frama-C
-option \lstinline+-cpp-extra-args <args>+ allows to pass \lstinline+<args>+
-at the end of the command for the first pass of the preprocessing.
-
-Example: In order to force \lstinline+gcc+ to include the header \lstinline+mylib.h+
-and to pre-process the annotations, the following command-line should be
-used:
-\begin{shell}
-frama-c-gui -eva -cpp-command 'gcc -C -E -I.' \
- -cpp-extra-args '-include mylib.h' \
- -pp-annot file1.c
-\end{shell}
+%% \question{In my annotations, macros are not pre-processed. What should
+%% I do?}
+
+%% The annotations being contained inside C comments, they
+%% {\it a priori} aren't affected by the preprocessing. It is possible
+%% to instruct Frama-C to launch the preprocessing on annotations
+%% with the option \lstinline|-pp-annot| (activated by default). Note that this option requires the
+%% preprocessor to be GNU \lstinline|cpp|, the GCC preprocessor\footnote{More
+%% precisely, the preprocessor must understand the {\tt -dD} and the
+%% {\tt -P} options that outputs macros definitions along with the
+%% pre-processed code and inhibits the generation of {\tt \#line}
+%% directives respectively.}.
+
+%% A typical example is as follows.
+%% \listinginputcaption{1}{\texttt{array.c}}{array.c}
+%% It is useful to use the pre-processor constant \lstinline|N|
+%% in the post-condition of function \lstinline|get_index()|.
+%% Use the command-line:
+%% \begin{shell}
+%% frama-c -eva array.c -pp-annot
+%% \end{shell}
+%% \medskip
+
+%% Note that when using this option, the preprocessing is
+%% made in two passes (the first
+%% pass operating on the code only, and the second operating on the
+%% annotations only). For this reason, the options passed to
+%% \lstinline|-cpp-command| in this case should only be commands that can
+%% be applied several times without ill side-effects. For instance,
+%% the \lstinline+-include+ option to \lstinline|cpp| is a command-line equivalent
+%% of the \lstinline+#include+ directive. If it was passed to \lstinline+cpp-command+
+%% while the preprocessing of annotations is being used, the
+%% corresponding header file would be included twice. The Frama-C
+%% option \lstinline+-cpp-extra-args <args>+ allows to pass \lstinline+<args>+
+%% at the end of the command for the first pass of the preprocessing.
+
+%% Example: In order to force \lstinline+gcc+ to include the header \lstinline+mylib.h+
+%% and to pre-process the annotations, the following command-line should be
+%% used:
+%% \begin{shell}
+%% frama-c-gui -eva -cpp-command 'gcc -C -E -I.' \
+%% -cpp-extra-args '-include mylib.h' \
+%% -pp-annot file1.c
+%% \end{shell}
\section*{Acknowledgments}
Dillon Pariente has provided helpful suggestions on this document
-since it was an early draft. I am especially thankful to him for
+since it was an early draft. We are especially thankful to him for
finding the courage to read it version after version.
Patrick Baudin, Richard Bonichon,
Jochen Burghardt,
G\'eraud Canet, Lo\"\i c Correnson,
David Delmas, Florent Kirchner, David Mentr\'e, Benjamin Monate, Anne Pacalet,
Julien Signoles provided useful comments in the process of
-getting the text to where it is today. Speaking of the text,
-I find awful, awkward constructs in it each time a
-new Frama-C release warrants a new pass on it. On the plus
-side, I am usually happy with it for a few days after each release,
-until I notice another blunder was left in.
-Do not hesitate to report documentation bugs
-at \url{http://bts.frama-c.com/main_page.php}.
+getting the text to where it is today.
+
+%Speaking of the text,
+%I find awful, awkward constructs in it each time a
+%new Frama-C release warrants a new pass on it. On the plus
+%side, I am usually happy with it for a few days after each release,
+%until I notice another blunder was left in.
+%Do not hesitate to report documentation bugs
+%at \url{http://bts.frama-c.com/main_page.php}.
%Illustrations were provided under the Creative Commons
%Attribution-Noncommercial-Share Alike license by members of the flickr
diff --git a/doc/value/tutorial/main_1.c b/doc/value/tutorial/main_1.c
index c27ad6e22c6e1991bd1aa2ea5b7eed1746addaf4..580dfb91ec4fd526f4319a8fa1caf8bd3da5f568 100644
--- a/doc/value/tutorial/main_1.c
+++ b/doc/value/tutorial/main_1.c
@@ -1,16 +1,15 @@
#include "skein.h"
+#include <stdio.h>
#define HASHLEN (8)
-int printf(const char*,...);
-
u08b_t msg[80]="People of Earth, your attention, please";
int main(void)
{
u08b_t hash[HASHLEN];
int i;
- Skein_256_Ctxt_t skein_context;
+ Skein_256_Ctxt_t skein_context;
Skein_256_Init( &skein_context, HASHLEN);
Skein_256_Update( &skein_context, msg, 80);
Skein_256_Final( &skein_context, hash);
diff --git a/opam/opam b/opam/opam
index 6d397bf21e359a873874cea691ddf2ca6a149489..7b2c44a9fa950c7f74182a16dd6bf4f04e6cd759 100644
--- a/opam/opam
+++ b/opam/opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "19.0.beta1"
+version: "19.0.beta2"
maintainer: "francois.bobot@cea.fr"
authors: [
"Michele Alberti"
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 023b14d756ba29bfdb59887a107e17a6915b6c1c..83eeb184084837fbf479bdf830bc4af2c8c1025f 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -521,19 +521,15 @@ struct
let unfold = ref (fun (_ : stmt) -> false)
- let printer =
- let pref : Printer.extensible_printer option ref = ref None in
- fun () ->
- match !pref with Some pp -> pp | None ->
- let pp = Printer.current_printer () in
- let module PP = (val pp: Printer.PrinterClass) in
- let module TAG = struct
- let create = T.create
- let unfold s = !unfold s
- end in
- let module TagPrinterClass = BUILD(TAG)(PP) in
- let printer = new TagPrinterClass.printer in
- pref := Some printer ; printer
+ let printer () =
+ let pp = Printer.current_printer () in
+ let module PP = (val pp: Printer.PrinterClass) in
+ let module TAG = struct
+ let create = T.create
+ let unfold s = !unfold s
+ end in
+ let module TagPrinterClass = BUILD(TAG)(PP) in
+ new TagPrinterClass.printer
let with_unfold_precond unfolder f fmt x =
let stack = !unfold in
diff --git a/src/plugins/gui/file_manager.ml b/src/plugins/gui/file_manager.ml
index ba532bf6bb70d030348711525496e36ee9584603..4edc958567c6e270a7c08fdbf2aa0687b5ac1588 100644
--- a/src/plugins/gui/file_manager.ml
+++ b/src/plugins/gui/file_manager.ml
@@ -243,13 +243,7 @@ let insert (host_window: Design.main_window_extension_points) =
[ Menu_manager.menubar ~icon:stock "Exit Frama-C"
(Menu_manager.Unit_callback Cmdline.bail_out) ]
in
- quit_item.(0)#add_accelerator `CONTROL 'q';
- ignore
- (menu_manager#add_entries
- filemenu
- ~pos:0
- [ Menu_manager.toolbar ~icon:stock ~label:"Exit" ~tooltip:"Exit Frama-C"
- (Menu_manager.Unit_callback Cmdline.bail_out)])
+ quit_item.(0)#add_accelerator `CONTROL 'q'
(** Register this dialog in main window menu bar *)
let () = Design.register_extension insert
diff --git a/src/plugins/gui/menu_manager.mli b/src/plugins/gui/menu_manager.mli
index 5c0ae0244b3315c05721bf88e6decf4b03012b87..bac69d4bc08f09138084f0e99b712b1b5ef27f8e 100644
--- a/src/plugins/gui/menu_manager.mli
+++ b/src/plugins/gui/menu_manager.mli
@@ -54,8 +54,8 @@ type entry = private {
(** {2 Smart constructors for menu entries.}
- If not supplied, the [active] parameter is the function that always returns
- [true].
+ If not supplied, the [sensitive] parameter is the function that always
+ returns [true].
@since Nitrogen-20111001 *)
val toolbar:
diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml
index 23a8ecc27f0dd7f4ebc02e4697896bd6fde88c3d..2e60e840184f5cee1e0b02eb2744304e7b43ffe3 100644
--- a/src/plugins/gui/project_manager.ml
+++ b/src/plugins/gui/project_manager.ml
@@ -23,10 +23,11 @@
let compare_prj (_p1, n1) (_p2, n2) =
String.compare n1 n2
-let projects_list () =
+let projects_list ?(filter=fun _ -> true) () =
let projects =
Project.fold_on_projects
- (fun acc p -> (p, Project.get_unique_name p) :: acc)
+ (fun acc p ->
+ if filter p then ((p, Project.get_unique_name p) :: acc) else acc)
[]
in
List.sort compare_prj projects
@@ -37,8 +38,8 @@ let projects_list () =
module PrjRadiosSet =
FCSet.Make
(struct
- type t = (Project.t * string) * GMenu.radio_menu_item
- let compare (p1, _) (p2, _) = compare_prj p1 p2
+ type t = (Project.t * string) * GButton.radio_button * GMenu.menu_item
+ let compare (p1, _, _) (p2, _, _) = compare_prj p1 p2
end)
let project_radios : PrjRadiosSet.t ref = ref PrjRadiosSet.empty
@@ -138,32 +139,19 @@ let load_project (host_window: Design.main_window_extension_points) =
| `DELETE_EVENT | `CANCEL -> ());
dialog#destroy ()
-let rename_project (main_ui: Design.main_window_extension_points) project =
- let old = Project.get_unique_name project in
- let s =
- Gtk_helper.input_string
- ~parent:main_ui#main_window
- ~title:"Renaming project"
- (Format.sprintf "New name for project %S:" old)
- in
- match s with
- | None -> ()
- | Some s ->
- try
- ignore (Project.from_unique_name s);
- main_ui#error "Project of name %S already exists" s
- with Project.Unknown_project ->
- Project.set_name project s
+let mk_project_markup p =
+ let name = Project.get_unique_name p in
+ if Project.is_current p then "<b>" ^ name ^ "</b>" else name
-let reset (menu: GMenu.menu) =
+let reset ?filter (menu: GMenu.menu) =
(* Do not reset all if there is no change. *)
- let pl = projects_list () in
+ let pl = projects_list ?filter () in
let same_projects =
(* use that project_radios and pl are sorted in the same way *)
try
let rest =
PrjRadiosSet.fold
- (fun (p1, _) acc ->
+ (fun (p1, _, _) acc ->
match acc with
| [] -> raise Exit
| p2 :: acc ->
@@ -178,65 +166,91 @@ let reset (menu: GMenu.menu) =
if same_projects then begin
(* update the item status according to the current project anyway *)
PrjRadiosSet.iter
- (fun ((p, _), r) -> r#set_active (Project.is_current p))
+ (fun ((p, _), r, i) ->
+ r#set_active (Project.is_current p);
+ let widgets = i#children in
+ match widgets with
+ | [ w ] ->
+ (try
+ let label = GMisc.label_cast w in
+ label#set_label (mk_project_markup p);
+ label#set_use_markup true
+ with Gobject.Cannot_cast (t1,t2) ->
+ Gui_parameters.warning
+ "Child of project menu item of kind %s while %s was expected"
+ t1 t2)
+ | [] -> Gui_parameters.warning "Project menu item without child"
+ | _ -> Gui_parameters.warning "Project menu item with %d child"
+ (List.length widgets)
+ )
!project_radios;
false
end else begin
- PrjRadiosSet.iter
- (fun (_, r) -> menu#remove (r :> GMenu.menu_item))
- !project_radios;
+ PrjRadiosSet.iter (fun (_, _, i) -> menu#remove i) !project_radios;
project_radios := PrjRadiosSet.empty;
true
end
-let rec duplicate_project window menu project =
- let new_p =
- Project.create_by_copy ~last:false ~src:project (Project.get_name project)
+let duplicate_project project =
+ ignore
+ (Project.create_by_copy ~last:false ~src:project (Project.get_name project))
+
+let rec rename_project
+ (main_ui: Design.main_window_extension_points) menu project
+ =
+ let old = Project.get_unique_name project in
+ let s =
+ Gtk_helper.input_string
+ ~parent:main_ui#main_window
+ ~title:"Renaming project"
+ (Format.sprintf "New name for project %S:" old)
in
- try
- (* update the menu *)
- let group =
- let _, i = PrjRadiosSet.choose !project_radios in
- i#group
- in
- ignore (mk_project_entry window menu ~group new_p)
- with Not_found ->
- (* menu not built (action called from the toolbar) *)
- ()
+ (match s with
+ | None -> ()
+ | Some s ->
+ try
+ ignore (Project.from_unique_name s);
+ main_ui#error "Project of name %S already exists" s
+ with Project.Unknown_project ->
+ Project.set_name project s);
+ recompute main_ui menu
and mk_project_entry window menu ?group p =
- let p_item = GMenu.radio_menu_item
+ let pname = Project.get_unique_name p in
+ let markup = mk_project_markup p in
+ let item = GMenu.menu_item ~packing:menu#append () in
+ let _label = GMisc.label ~markup ~xalign:0. ~packing:item#add () in
+ let submenu = GMenu.menu ~packing:item#set_submenu () in
+ let current = GMenu.menu_item ~packing:submenu#append () in
+ let p_item = GButton.radio_button
?group
~active:(Project.is_current p)
- ~packing:menu#append
+ ~packing:current#add
+ ~label:"Set current"
()
in
- let callback () = if p_item#active then Project.set_current p in
- let pname = Project.get_unique_name p in
- ignore (p_item#connect#toggled ~callback);
- project_radios := PrjRadiosSet.add ((p, pname), p_item) !project_radios;
- let box = GPack.hbox ~packing:p_item#add () in
- ignore (GMisc.label ~text:pname ~packing:box#pack ());
- let buttons_box = GPack.hbox ~packing:(box#pack ~from:`END) () in
+ let callback () = Project.set_current p in
+ ignore (current#connect#activate ~callback);
+ project_radios := PrjRadiosSet.add ((p, pname), p_item, item) !project_radios;
let add_action stock text callback =
- let item = GButton.button ~packing:buttons_box#pack () in
- Gtk_helper.do_tooltip ~tooltip:text item;
- item#set_relief `NONE;
- let image = GMisc.image ~stock () in
- item#set_image image#coerce;
- image#set_icon_size `MENU;
- ignore (item#connect#clicked ~callback)
+ let image = GMisc.image ~xalign:0. ~stock () in
+ let image = image#coerce in
+ let item =
+ Gtk_helper.image_menu_item ~image ~text ~packing:submenu#append
+ in
+ ignore (item#connect#activate ~callback)
in
add_action `COPY "Duplicate project"
- (fun () -> duplicate_project window menu p);
+ (fun () -> duplicate_project p);
add_action `DELETE "Delete project" (fun () -> delete_project p);
add_action `SAVE "Save project" (fun () -> save_project window p);
add_action `SAVE_AS "Save project as" (fun () -> save_project_as window p);
- add_action `SELECT_FONT "Rename project" (fun () -> rename_project window p);
+ add_action
+ `SELECT_FONT "Rename project" (fun () -> rename_project window menu p);
p_item
-let make_project_entries window menu =
- match projects_list () with
+and make_project_entries ?filter window menu =
+ match projects_list ?filter () with
| [] -> assert false
| (pa, _name) :: tl ->
let mk = mk_project_entry window menu in
@@ -244,6 +258,10 @@ let make_project_entries window menu =
let group = pa_item#group in
List.iter (fun (pa, _) -> ignore (mk ~group pa)) tl
+and recompute ?filter window menu =
+ let is_reset = reset ?filter menu in
+ if is_reset then make_project_entries ?filter window menu
+
open Menu_manager
(** Register this dialog in main window menu bar *)
@@ -251,7 +269,7 @@ let () =
Design.register_extension
(fun window ->
let menu_manager = window#menu_manager () in
- let item, menu = menu_manager#add_menu "_Project" in
+ let _item, menu = menu_manager#add_menu "_Project" in
let constant_items =
menu_manager#add_entries
menu
@@ -262,23 +280,30 @@ let () =
(Unit_callback (fun () -> load_project window));
menubar ~icon:`COPY "Duplicate current project"
(Unit_callback
- (fun () -> duplicate_project window menu(Project.current())));
+ (fun () -> duplicate_project (Project.current())));
menubar ~icon:`DELETE "Delete current project"
(Unit_callback (fun () -> delete_project (Project.current ())));
menubar ~icon:`SELECT_FONT "Rename current project"
(Unit_callback
- (fun () -> rename_project window (Project.current ())));
+ (fun () -> rename_project window menu (Project.current ())));
]
in
let new_item = constant_items.(0) in
new_item#add_accelerator `CONTROL 'n';
constant_items.(3)#add_accelerator `CONTROL 'd';
ignore (GMenu.separator_item ~packing:menu#append ());
- let callback () =
- let is_reset = reset menu in
- if is_reset then make_project_entries window menu
+ let callback_prj _p = recompute window menu in
+ let callback_rm_prj p =
+ let filter p' = not (Project.equal p p') in
+ recompute ~filter window menu
in
- ignore (item#connect#activate ~callback))
+ let hook () = recompute window menu in
+ Project.register_create_hook callback_prj;
+ Project.register_after_set_current_hook ~user_only:true callback_prj;
+ Project.register_before_remove_hook callback_rm_prj;
+ Project.register_after_load_hook hook;
+ Project.register_after_global_load_hook hook;
+ recompute window menu)
(*
Local Variables:
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index a62ca61f74f49ede1bd466217377af4d37ba2a55..66564553c4f4b958928c1fd55a637749e6800424 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -252,9 +252,9 @@ let register_builtin_comparison suffix ft =
add_builtin ("\\ge_" ^ suffix) signature ge ;
Context.register
begin fun () ->
- let compute phi x y = e_fun phi [y;x] in
- Lang.F.set_builtin_2 gt (compute (flt_lt ft)) ;
- Lang.F.set_builtin_2 ge (compute (flt_le ft)) ;
+ let converse phi x y = e_fun phi [y;x] in
+ Lang.F.set_builtin_2 gt (converse (flt_lt ft)) ;
+ Lang.F.set_builtin_2 ge (converse (flt_le ft)) ;
end
end
diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index d1c55685ea4d7add16b3f3e43080df932afe60c3..44e1686bff264800432a447e2dc2069f62f16e8a 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -188,13 +188,18 @@ struct
| C_int i -> Val (iop i (val_of_exp env e1) (val_of_exp env e2))
| _ -> assert false
- let bool_of_comp env iop lop e1 e2 =
+ let bool_of_comp env iop lop fop e1 e2 =
let t1 = Cil.typeOf e1 in
let t2 = Cil.typeOf e2 in
if Cil.isPointerType t1 && Cil.isPointerType t2 then
Cvalues.is_true (lop (loc_of_exp env e1) (loc_of_exp env e2))
- else
- iop (val_of_exp env e1) (val_of_exp env e2)
+ else match Cil.unrollType t1 with
+ | TFloat(f,_) ->
+ let p = fop (Ctypes.c_float f)
+ (val_of_exp env e1) (val_of_exp env e2) in
+ e_if (F.e_prop p) e_one e_zero
+ | _ ->
+ iop (val_of_exp env e1) (val_of_exp env e2)
let bool_of_exp env e =
match Ctypes.object_of (Cil.typeOf e) with
@@ -214,12 +219,12 @@ struct
| BAnd -> arith_int env tr Cint.band e1 e2
| BOr -> arith_int env tr Cint.bor e1 e2
| BXor -> arith_int env tr Cint.bxor e1 e2
- | Eq -> Val (bool_of_comp env Cvalues.bool_eq M.loc_eq e1 e2)
- | Ne -> Val (bool_of_comp env Cvalues.bool_neq M.loc_neq e1 e2)
- | Lt -> Val (bool_of_comp env Cvalues.bool_lt M.loc_lt e1 e2)
- | Gt -> Val (bool_of_comp env Cvalues.bool_lt M.loc_lt e2 e1)
- | Le -> Val (bool_of_comp env Cvalues.bool_leq M.loc_leq e1 e2)
- | Ge -> Val (bool_of_comp env Cvalues.bool_leq M.loc_leq e2 e1)
+ | Eq -> Val (bool_of_comp env Cvalues.bool_eq M.loc_eq Cfloat.feq e1 e2)
+ | Ne -> Val (bool_of_comp env Cvalues.bool_neq M.loc_neq Cfloat.fneq e1 e2)
+ | Lt -> Val (bool_of_comp env Cvalues.bool_lt M.loc_lt Cfloat.flt e1 e2)
+ | Gt -> Val (bool_of_comp env Cvalues.bool_lt M.loc_lt Cfloat.flt e2 e1)
+ | Le -> Val (bool_of_comp env Cvalues.bool_leq M.loc_leq Cfloat.fle e1 e2)
+ | Ge -> Val (bool_of_comp env Cvalues.bool_leq M.loc_leq Cfloat.fle e2 e1)
| LAnd -> Val (Cvalues.bool_and (bool_of_exp env e1) (bool_of_exp env e2))
| LOr -> Val (Cvalues.bool_or (bool_of_exp env e1) (bool_of_exp env e2))
| PlusPI | IndexPI ->
diff --git a/src/plugins/wp/GuiConfig.ml b/src/plugins/wp/GuiConfig.ml
index 51eb58da11637ed283a1dc370c84aafbeadfe1e2..6e92c3e98ec00f2563539dffde0e9119e458270c 100644
--- a/src/plugins/wp/GuiConfig.ml
+++ b/src/plugins/wp/GuiConfig.ml
@@ -181,7 +181,7 @@ class dp_button ~(available:available) =
| [] -> ERGO
| spec::others ->
match VCS.prover_of_name spec with
- | None | Some (Why3ide|Qed) -> NONE
+ | None | Some Qed -> NONE
| Some (AltErgo|Tactical) -> ERGO
| Some Coq -> COQ
| Some (Why3 s) ->
diff --git a/src/plugins/wp/GuiList.ml b/src/plugins/wp/GuiList.ml
index 19e5a4fdd7ed853316e83b42b7dcbdae2a301329..c9f72fcb75347e219a9100376a3f6afdaeabfc04 100644
--- a/src/plugins/wp/GuiList.ml
+++ b/src/plugins/wp/GuiList.ml
@@ -147,7 +147,7 @@ class pane (enabled:GuiConfig.enabled) =
ignore (list#add_column_text ~title:"Model" [] render) ;
List.iter
self#create_prover
- [ VCS.Qed ; VCS.Tactical ; VCS.AltErgo ; VCS.Coq ; VCS.Why3ide ] ;
+ [ VCS.Qed ; VCS.Tactical ; VCS.AltErgo ; VCS.Coq ] ;
ignore (list#add_column_empty) ;
list#set_selection_mode `MULTIPLE ;
enabled#connect self#configure ;
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 28bb37c4c63cf8326a3e6cb7f56a4a5ff89b67e0..5862f52bcd7d5e69f0583f5e2d73fe1247844ed2 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -239,9 +239,11 @@ class behavior
Task.spawn server thread ;
Task.launch server in
match prover with
+ (*
| VCS.Why3ide ->
let iter f = Wpo.iter ~on_goal:f () in
schedule (ProverWhy3ide.prove ~callback:result ~iter)
+ *)
| VCS.Tactical ->
begin
match mode , ProverScript.get w with
@@ -301,12 +303,12 @@ class behavior
match popup_target with
| Some(w,Some p) -> (popup_target <- None ; self#prove ~mode w p)
| _ -> popup_target <- None
-
+(*
method private popup_why3ide () =
match popup_target with
| Some(w,_) -> (popup_target <- None ; self#prove w VCS.Why3ide)
| _ -> popup_target <- None
-
+*)
method private add_popup_delete popup =
begin
popup#add_separator ;
@@ -331,11 +333,13 @@ class behavior
[ "Run",BatchMode ; "Open Altgr-Ergo on Fail",EditMode ; "Open Altgr-Ergo",EditMode ] ;
self#add_popup_proofmodes popup_coq
[ "Check Proof",BatchMode ; "Edit on Fail",EditMode ; "Edit Proof",EditMode ] ;
+ (*
List.iter
(fun menu ->
menu#add_item ~label:"Open Why3ide" ~callback:self#popup_why3ide ;
self#add_popup_delete menu ;
) [ popup_qed ; popup_why3 ; popup_ergo ; popup_coq ] ;
+ *)
end
method private popup w p =
@@ -344,7 +348,7 @@ class behavior
popup_target <- Some (w,p) ;
match p with
| None | Some Tactical -> popup_tip#run ()
- | Some (Qed|Why3ide) -> popup_qed#run ()
+ | Some Qed -> popup_qed#run ()
| Some Coq -> popup_coq#run ()
| Some AltErgo -> popup_ergo#run ()
| Some (Why3 _) -> popup_why3#run ()
diff --git a/src/plugins/wp/GuiProver.ml b/src/plugins/wp/GuiProver.ml
index 1ed614ee5f2eab4fb5e7a1d5813a17ac5a3caf8c..12301055031fc7542f127790f6edbc1fd4db9b3b 100644
--- a/src/plugins/wp/GuiProver.ml
+++ b/src/plugins/wp/GuiProver.ml
@@ -26,7 +26,7 @@ let ko_status = `Share "theme/default/unknown.png"
let wg_status = `Share "theme/default/invalid.png"
let filter = function
- | VCS.Qed | VCS.Tactical | VCS.Why3ide | VCS.Coq -> false
+ | VCS.Qed | VCS.Tactical | VCS.Coq -> false
| VCS.Why3 _ | VCS.AltErgo -> true
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 2c8f9c8028b3f78ca70d4d6b57f46f9b2641ea2f..a068ad272fde2482a8e4866ff2ab5f631894f6ab 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -295,6 +295,7 @@ struct
| EQ_set
| EQ_loc
| EQ_plain
+ | EQ_float of c_float
| EQ_array of Matrix.matrix
| EQ_comp of compinfo
| EQ_incomparable
@@ -306,7 +307,8 @@ struct
| Ctype t ->
match Ctypes.object_of t with
| C_pointer _ -> EQ_loc
- | C_int _ | C_float _ -> EQ_plain
+ | C_int _ -> EQ_plain
+ | C_float f -> EQ_float f
| C_comp c -> EQ_comp c
| C_array a -> EQ_array (Matrix.of_array a)
@@ -323,6 +325,7 @@ struct
| None -> EQ_incomparable
else EQ_incomparable
| EQ_plain , EQ_plain -> EQ_plain
+ | EQ_float f1 , EQ_float f2 when f1 = f2 -> EQ_float f1
| _ -> EQ_incomparable
let use_equal = function
@@ -357,6 +360,9 @@ struct
then p_equal va vb
else Cvalues.equal_array m va vb
+ | EQ_float f ->
+ Cfloat.feq f (val_of_term env a) (val_of_term env b)
+
| EQ_plain ->
p_equal (val_of_term env a) (val_of_term env b)
@@ -370,11 +376,21 @@ struct
let term_diff polarity env a b =
p_not (term_equal (Cvalues.negate polarity) env a b)
- let compare_term env vrel lrel a b =
+
+ let float_of_logic_type lt =
+ match Logic_utils.unroll_type lt with
+ | Ctype ty ->
+ (match Cil.unrollType ty with
+ | TFloat(f,_) -> Some (Ctypes.c_float f)
+ | _ -> None)
+ | _ -> None
+
+ let compare_term env vrel lrel frel a b =
if Logic_typing.is_pointer_type a.term_type then
lrel (loc_of_term env a) (loc_of_term env b)
- else
- vrel (val_of_term env a) (val_of_term env b)
+ else match float_of_logic_type a.term_type with
+ | Some f -> frel f (val_of_term env a) (val_of_term env b)
+ | None -> vrel (val_of_term env a) (val_of_term env b)
(* -------------------------------------------------------------------------- *)
(* --- Term Comparison --- *)
@@ -386,8 +402,8 @@ struct
let exp_diff env a b =
Vexp(e_prop (term_diff `NoPolarity env a b))
- let exp_compare env vrel lrel a b =
- Vexp(e_prop (compare_term env vrel lrel a b))
+ let exp_compare env vrel lrel frel a b =
+ Vexp(e_prop (compare_term env vrel lrel frel a b))
(* -------------------------------------------------------------------------- *)
(* --- Binary Operators --- *)
@@ -443,10 +459,10 @@ struct
| BOr -> L.apply Cint.l_or (C.logic env a) (C.logic env b)
| LAnd -> Vexp(e_and (List.map (val_of_term env) (fold_assoc LAnd [] [a;b])))
| LOr -> Vexp(e_or (List.map (val_of_term env) (fold_assoc LOr [] [a;b])))
- | Lt -> exp_compare env p_lt M.loc_lt a b
- | Gt -> exp_compare env p_lt M.loc_lt b a
- | Le -> exp_compare env p_leq M.loc_leq a b
- | Ge -> exp_compare env p_leq M.loc_leq b a
+ | Lt -> exp_compare env p_lt M.loc_lt Cfloat.flt a b
+ | Gt -> exp_compare env p_lt M.loc_lt Cfloat.flt b a
+ | Le -> exp_compare env p_leq M.loc_leq Cfloat.fle a b
+ | Ge -> exp_compare env p_leq M.loc_leq Cfloat.fle b a
| Eq -> exp_equal env a b
| Ne -> exp_diff env a b
@@ -779,10 +795,10 @@ struct
let relation polarity env rel a b =
match rel with
- | Rlt -> compare_term env p_lt M.loc_lt a b
- | Rgt -> compare_term env p_lt M.loc_lt b a
- | Rle -> compare_term env p_leq M.loc_leq a b
- | Rge -> compare_term env p_leq M.loc_leq b a
+ | Rlt -> compare_term env p_lt M.loc_lt Cfloat.flt a b
+ | Rgt -> compare_term env p_lt M.loc_lt Cfloat.flt b a
+ | Rle -> compare_term env p_leq M.loc_leq Cfloat.fle a b
+ | Rge -> compare_term env p_leq M.loc_leq Cfloat.fle b a
| Req -> term_equal polarity env a b
| Rneq -> term_diff polarity env a b
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 61230201355a42ea080a7dcd676971d9832c62cf..6c92361439bfb00f0bca1fcd47263e867a96d920 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -392,7 +392,7 @@ let assemble_wpo wpo =
end
| Wpo.Function (kf,_behv) ->
let model = Model.get_model () in
- let file = Wpo.DISK.file_kf ~kf ~model ~prover:VCS.Why3ide in
+ let file = Wpo.DISK.file_kf ~kf ~model ~prover:(VCS.Why3 "") in
let age = try FunFile.find kf with Not_found -> -1 in
begin if age < Wpo.age wpo then
let age_max = ref (-1) in
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 55503473e6756ac20edb0b964c66418b6cb230f0..a66cdf5321f7905578151da8d263fc024f254772 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -31,7 +31,7 @@ let dkey_success_only = Wp_parameters.register_category "success-only"
type prover =
| Why3 of string (* Prover via WHY *)
- | Why3ide
+ (* | Why3ide *)
| AltErgo (* Alt-Ergo *)
| Coq (* Coq and Coqide *)
| Qed (* Qed Solver *)
@@ -54,16 +54,16 @@ let prover_of_name = function
| "coq" | "coqide" -> Some Coq
| "script" -> Some Tactical
| "tip" -> Some Tactical
- | "why3ide" -> Some Why3ide
+ (* | "why3ide" -> Some Why3ide *)
| s ->
match Extlib.string_del_prefix "why3:" s with
| Some "" -> None
- | Some "ide" -> Some Why3ide
+ (* | Some "ide" -> Some Why3ide*)
| Some s' -> Some (Why3 s')
| None -> Some (Why3 s)
let name_of_prover = function
- | Why3ide -> "why3ide"
+ (* | Why3ide -> "why3ide" *)
| Why3 s -> "why3:" ^ s
| AltErgo -> "alt-ergo"
| Coq -> "coq"
@@ -75,7 +75,7 @@ let title_of_prover = function
| Why3 "z3" -> "Z3"
| Why3 ("alt-ergo" | "altergo") -> "Alt-Ergo (why3)"
| Why3 s -> Printf.sprintf "Why3 (%s)" s
- | Why3ide -> "Why3 (ide)"
+ (* | Why3ide -> "Why3 (ide)" *)
| AltErgo -> "Alt-Ergo"
| Coq -> "Coq"
| Qed -> "Qed"
@@ -102,7 +102,7 @@ let sanitize_why3 s =
let filename_for_prover = function
| Why3 s -> sanitize_why3 s
- | Why3ide -> "Why3_ide"
+ (* | Why3ide -> "Why3_ide" *)
| AltErgo -> "Alt-Ergo"
| Coq -> "Coq"
| Qed -> "Qed"
@@ -110,7 +110,7 @@ let filename_for_prover = function
let language_of_prover = function
| Why3 _ -> L_why3
- | Why3ide -> L_why3
+ (* | Why3ide -> L_why3 *)
| Coq -> L_coq
| AltErgo -> L_altergo
| Qed | Tactical -> L_why3
@@ -128,7 +128,7 @@ let mode_of_prover_name = function
let is_auto = function
| Qed | AltErgo | Why3 _ -> true
- | Tactical | Why3ide | Coq -> false
+ | Tactical | Coq -> false
let cmp_prover p q =
match p,q with
@@ -145,13 +145,9 @@ let cmp_prover p q =
| Coq , _ -> (-1)
| _ , Coq -> 1
| Why3 p , Why3 q -> String.compare p q
- | Why3 _, _ -> (-1)
- | _, Why3 _ -> 1
- | Why3ide, Why3ide -> 0
let pp_prover fmt = function
| AltErgo -> Format.pp_print_string fmt "Alt-Ergo"
- | Why3ide -> Format.pp_print_string fmt "Why3ide"
| Coq -> Format.pp_print_string fmt "Coq"
| Why3 smt ->
if Wp_parameters.debug_atleast 1 then
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 7d9eb27c8d224079b9b15ff9d151f0b8fce7b1fd..fb29085fdb99139307d7e52905a504ffb7e11036 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -28,7 +28,6 @@
type prover =
| Why3 of string (* Prover via WHY *)
- | Why3ide
| AltErgo (* Alt-Ergo *)
| Coq (* Coq and Coqide *)
| Qed (* Qed Solver *)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index f1970bf98877f1dcc5e6182448ce166f374bc115..b20427d8549f8af88dcb751ba51374eb1940ea54 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -988,7 +988,7 @@ controlled by the following options:
(default is: \texttt{1000}).
\end{description}
-\subsection{Decision Procedures Interface}
+\subsection{Prover Selection}
\label{wp-provers}
The generated proof obligations are submitted to external decision
@@ -1103,41 +1103,69 @@ then save the proof scripts in order to replay them in batch mode.
\item[\tt -wp-coq-project='<name>'] override the \verb+_CoqProject+ file name
for Emacs and Proof General.
\end{description}
-
\hrule
-\paragraph{Why3.}
-Since \textsf{WP} version \verb+0.7+ (Fluorine), native support for \textsf{Why3}
-and \textsf{Why3-Ide} are provided. The older system \textsf{Why}
-\verb+2.x+ is \emph{no} longer supported.
+
+\pagebreak
+\paragraph{Why-3.}
+Native support for \textsf{Why-3} is provided (for versions 1.0 and newer).
+\\
+Support for \textsf{Why-3 IDE} is no longer provided.
\begin{description}
-\item[\tt -wp-prover "why3ide"] runs \textsf{Why3-Ide} with all
- generated goals. On exit, the \textsf{WP} plug-in reads back your
- \textsf{Why3} session and updates the proof obligation status accordingly.
-\item[\tt -wp-prover "<p>"] runs a \textsf{Why3} prover named \texttt{<p>}.
-\item[\tt -wp-prover "why3:<p>"] useful alias when \texttt{"<p>"} can
- be ambiguous. It is actually different to run \texttt{alt-ergo} or \texttt{coq}
- directly from \textsf{WP} or through \textsf{Why3}.
-\item[\tt -wp-detect] lists the provers available with \textsf{Why3}.
- This command calls \texttt{why3 --list-provers} but you have to
- configure \textsf{Why3} on your own before, for instance by using
- \texttt{why3config}. Consult the \textsf{Why3} user manual for details.
- The listed prover names can be directly used with the \texttt{-wp-prover} option.
-\item[\tt -wp-why3='<cmd>'] override the \verb+why3+ command.
+\item[\tt -wp-prover "why3:<p>"] runs a \textsf{Why-3} prover named \texttt{<p>}, and
+ exactly behaves like invoking \verb+why3 prover -P <p>+. The list of prover
+ names \verb+<p>+ must be extracted from the \verb+[alias]+ section of your \textsf{Why-3}
+ configuration, which \verb+frama-c -wp-detect+ does for you (see below).
+\item[\tt -wp-prover "<p>"] can also be used instead of \verb+-wp-prover "why3:<p>"+
+ when \verb+<p>+ is not natively supported by \textsf{WP}, like \texttt{alt-ergo},
+ \texttt{altgr-ergo}, \texttt{coq}, \texttt{coqide}, \texttt{script} and \texttt{tip}.
+\item[\tt -wp-detect] lists the provers available for \textsf{Why-3}.
+ This command can only work if \textsf{why3} API was installed before building and
+ installing \textsf{Frama-C}.
+ The option reads your \textsf{Why-3} configuration and prints the available
+ provers with their \verb+-wp-prover <p>+ code names.
+\item[\tt -wp-why3='<cmd>'] overrides the path to the \verb+why3+ command.
\end{description}
-\paragraph{Sessions.}
-Your \textsf{Why3} session is saved in the \texttt{"project.session"}
-sub-directory of \texttt{-wp-out}. You may run
-\texttt{why3ide} by hand by issuing the following command:
-\begin{shell}
-# why3ide -I <frama-c-share>/wp <out>/project.session
-\end{shell}
+\paragraph{Example of using Why-3.}
+Suppose you have the following configuration:
+
+\begin{logs}
+# frama-c -wp-detect
+[wp] Why3 provers detected:
+ - Alt-Ergo 2.0.0 [why3:alt-ergo,altergo]
+ - CVC4 1.6 [cvc4]
+ - CVC4 1.6 (counterexamples) [cvc4-ce]
+ - Coq 8.9.0 [why3:coq]
+ - Z3 4.6.0 [z3]
+ - Z3 4.6.0 (counterexamples) [z3-ce]
+ - Z3 4.6.0 (noBV) [z3-nobv]
+\end{logs}
-Proof recovering features of \textsf{Why3} are fully available, and
-you can interleave proving from \textsf{WP} with manual runs of
-\texttt{why3ide}. Interactive proofs with \textsf{Why3} are completely
-separated from those managed by the native \textsf{WP} interface with
-\textsf{Coq}.
+Then, to use (for instance) \textsf{CVC4 1.6},
+you can use \verb+-wp-prover cvc4+ (since this name is not conflicting
+with any native prover). Alternatively, you can also use the less ambiguous
+name \verb+-wp-prover why3:cvc4+ if you prefer.
+Similarly, if you want to use \textsf{Z3 4.6.0} without bitvectors, you can use \verb+-wp-prover z3-nobv+
+or \verb+-wp-prover why3:z3-nobv+.
+
+However, to use \textsf{Alt-Ergo 2.0.0} \emph{via} \textsf{Why-3}, you shall use
+\verb+-wp-prover why3:alt-ergo+, since \verb+-wp-prover alt-ergo+ would select
+the native support of \textsf{Alt-Ergo} prover. Finally, since \textsf{Why-3} also provides the alias
+\verb+altergo+ for this prover, \verb+-wp-prover altergo+ will also run it \emph{via} \textsf{Why-3}.
+
+%% \paragraph{Sessions.}
+%% Your \textsf{Why3} session is saved in the \texttt{"project.session"}
+%% sub-directory of \texttt{-wp-out}. You may run
+%% \texttt{why3ide} by hand by issuing the following command:
+%% \begin{shell}
+%% # why3ide -I <frama-c-share>/wp <out>/project.session
+%% \end{shell}
+
+%% Proof recovering features of \textsf{Why3} are fully available, and
+%% you can interleave proving from \textsf{WP} with manual runs of
+%% \texttt{why3ide}. Interactive proofs with \textsf{Why3} are completely
+%% separated from those managed by the native \textsf{WP} interface with
+%% \textsf{Coq}.
\subsection{Generated Proof Obligations}
Your proof obligations are generated and saved to several text
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index bc18054056ee79ce17a0b201df3c98f2e3c78cb5..530e74c3d0f64be6e5b0fe16ba8c15cc93921d70 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -36,7 +36,6 @@ let dispatch ?(config=VCS.default) mode prover wpo =
| Coq -> ProverCoq.prove mode wpo
| Why3 prover -> ProverWhy3.prove ?timeout:config.timeout ~prover wpo
| Qed | Tactical -> Task.return VCS.no_result
- | _ -> Task.failed "Prover '%a' not available" VCS.pp_prover prover
end
let started ?start wpo =
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index ad824c977d63875b53b78de4814e3d564ae4d038..f17abda0620a3a385be354a642079943e11a644a 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -513,8 +513,10 @@ let compute_provers ~mode =
(fun pname prvs ->
match VCS.prover_of_name pname with
| None -> prvs
+ (*
| Some VCS.Why3ide ->
mode.why3ide <- true; prvs
+ *)
| Some VCS.Tactical ->
mode.tactical <- true ;
if pname = "tip" then mode.update <- true ;
@@ -626,8 +628,10 @@ let do_wp_proofs_iter iter =
let spawned = mode.why3ide || mode.tactical || mode.provers <> [] in
begin
if spawned then do_list_scheduled iter ;
+ (*
if mode.why3ide then
launch (ProverWhy3ide.prove ~callback:do_why3_result ~iter) ;
+ *)
spawn_wp_proofs_iter ~mode iter ;
if spawned then
begin
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index fee194ce70ab07b10bf6bdf595543c7b59b09f82..ac921a318be08275381f558f6f55e0a47a049d54 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -13,7 +13,7 @@
[wp] [Qed] Goal typed_call_main_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_call_main_call_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
-[wp] [Alt-Ergo] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
+[wp] [Alt-Ergo] Goal typed_double_call_call_f_2_requires_qed_ok_Rf : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_main_ensures_qed_ok_Emain : Valid
[wp] [Qed] Goal typed_main_call_f_requires_qed_ok_Rf : Valid
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index 320ad154cdac77a26b1768685510442f460ebc05..ae5dcae5a7fcbf01f1c728a8947e98dc0deb6944 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
@@ -24,7 +24,7 @@ let run () =
List.fold_right
(fun pname prvs -> match VCS.prover_of_name pname with
| None -> prvs
- | Some VCS.Why3ide | Some VCS.Tactical -> prvs
+ | Some VCS.Tactical -> prvs
| Some prv -> (VCS.mode_of_prover_name pname, prv) :: prvs)
["qed"] []
in
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index a10fb172d38336400c6fc3eb46e0ca9acd6f0916..ae0f98a6d4a7abfcd196df32c00668ce32545ea7 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -23,7 +23,7 @@ let run () =
List.fold_right
(fun pname prvs -> match VCS.prover_of_name pname with
| None -> prvs
- | Some VCS.Why3ide | Some VCS.Tactical -> prvs
+ | Some VCS.Tactical -> prvs
| Some prv -> (VCS.mode_of_prover_name pname, prv) :: prvs)
["alt-ergo"] []
in
diff --git a/src/plugins/wp/tests/wp_acsl/float_compare.i b/src/plugins/wp/tests/wp_acsl/float_compare.i
index 3e039b2cb13d4b139990011bfb807323d54d3c8f..6abdcffafafa069a0139033e6fd83e41313f8e29 100644
--- a/src/plugins/wp/tests/wp_acsl/float_compare.i
+++ b/src/plugins/wp/tests/wp_acsl/float_compare.i
@@ -1,3 +1,7 @@
+/* run.config_qualif
+ OPT: -wp-prover why3:alt-ergo
+ */
+
/*@ lemma test_float_compare:
\forall float x,y;
\is_finite(x) && \is_finite(y) ==>
@@ -21,3 +25,47 @@
\is_finite(x) && \is_finite(y) ==> \ge_double(x,y) ==>
\gt_double(x,y) || \eq_double(x,y);
*/
+
+/*@ lemma finite_32_64:
+ \forall float x;
+ \is_finite(x) ==> \is_finite((double)x);
+*/
+
+/*@ lemma finite_32_64_real:
+ \forall float x;
+ \is_finite(x) ==> ((real) x) == ((real)(double) x) ;
+*/
+
+/*@
+ requires \is_finite(a) && \is_finite(b);
+ ensures DEF: \result == ((a < b) ? 1 : 0) ;
+ ensures REL1: \result <==> a < b ;
+ ensures REL2: \result <==> a < b ;
+*/
+int cmp_ff(float a,float b) { return a < b; }
+
+/*@
+ requires \is_finite(a) && \is_finite(b);
+ ensures DEF: \result == ((a < b) ? 1 : 0) ;
+ ensures REL1: \result <==> a < b ;
+ ensures REL2: \result <==> a < b ;
+*/
+int cmp_dd(double a,double b) { return a < b; }
+
+/*@
+ requires \is_finite(a) && \is_finite(b);
+ ensures DEF: \result == ((a < b) ? 1 : 0) ;
+ ensures REL1: \result <==> a < b ;
+ ensures REL2: \result <==> a < b ;
+*/
+int cmp_fd(float a,double b) {
+ //@ assert \is_finite((double)a);
+ //@ assert ((real) a) == ((real)(double)a) ;
+ return a < b;
+}
+
+/*@
+ ensures POS: \lt_float(a,b) <==> \result == 1 ;
+ ensures NEG: !\lt_float(a,b) <==> \result == 0 ;
+*/
+int cmp_fnan(float a,float b) { return a < b; }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
index a31e1893ff76431ccf8b5d83313080b8d476d614..0fc794250f024d6e9e85362c6e510e2ef6e11813 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
@@ -2,10 +2,26 @@
[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
------------------------------------------------------------
Global
------------------------------------------------------------
+Lemma finite_32_64:
+Assume: 'test_double_compare_greater' 'test_float_compare_greater'
+ 'test_double_compare' 'test_float_compare'
+Prove: (is_finite_f32 x_0) -> (is_finite_f64 (to_f64 (of_f32 x_0)))
+
+------------------------------------------------------------
+
+Lemma finite_32_64_real:
+Assume: 'finite_32_64' 'test_double_compare_greater'
+ 'test_float_compare_greater' 'test_double_compare' 'test_float_compare'
+Prove: let r_0 = (of_f32 x_0) in
+ (is_finite_f32 x_0) -> ((of_f64 (to_f64 r_0))=r_0)
+
+------------------------------------------------------------
+
Lemma test_double_compare:
Assume: 'test_float_compare'
Prove: (is_finite_f64 x_0) -> (is_finite_f64 y_0) -> (le_f64 x_0 y_0)
@@ -33,3 +49,128 @@ Prove: (is_finite_f32 x_0) -> (is_finite_f32 y_0) -> (le_f32 y_0 x_0)
-> ((eq_f32 x_0 y_0) \/ (lt_f32 y_0 x_0))
------------------------------------------------------------
+------------------------------------------------------------
+ Function cmp_dd
+------------------------------------------------------------
+
+Goal Post-condition 'DEF' in 'cmp_dd':
+Assume { (* Pre-condition *) Have: is_finite_f64(a) /\ is_finite_f64(b). }
+Prove: (if lt_f64b(a, b) then 1 else 0)
+ = (if (of_f64(a) < of_f64(b)) then 1 else 0).
+
+------------------------------------------------------------
+
+Goal Post-condition 'REL1' in 'cmp_dd':
+Assume { (* Pre-condition *) Have: is_finite_f64(a) /\ is_finite_f64(b). }
+Prove: lt_f64(a, b) <-> (of_f64(a) < of_f64(b)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'REL2' in 'cmp_dd':
+Assume { (* Pre-condition *) Have: is_finite_f64(a) /\ is_finite_f64(b). }
+Prove: lt_f64(a, b) <-> (of_f64(a) < of_f64(b)).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function cmp_fd
+------------------------------------------------------------
+
+Goal Post-condition 'DEF' in 'cmp_fd':
+Let r = of_f32(a).
+Let a_1 = to_f64(r).
+Assume {
+ (* Pre-condition *)
+ Have: is_finite_f32(a) /\ is_finite_f64(b).
+ (* Assertion *)
+ Have: is_finite_f64(a_1).
+ (* Assertion *)
+ Have: of_f64(a_1) = r.
+}
+Prove: (if lt_f64b(a_1, b) then 1 else 0)
+ = (if (r < of_f64(b)) then 1 else 0).
+
+------------------------------------------------------------
+
+Goal Post-condition 'REL1' in 'cmp_fd':
+Let r = of_f32(a).
+Let a_1 = to_f64(r).
+Assume {
+ (* Pre-condition *)
+ Have: is_finite_f32(a) /\ is_finite_f64(b).
+ (* Assertion *)
+ Have: is_finite_f64(a_1).
+ (* Assertion *)
+ Have: of_f64(a_1) = r.
+}
+Prove: lt_f64(a_1, b) <-> (r < of_f64(b)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'REL2' in 'cmp_fd':
+Let r = of_f32(a).
+Let a_1 = to_f64(r).
+Assume {
+ (* Pre-condition *)
+ Have: is_finite_f32(a) /\ is_finite_f64(b).
+ (* Assertion *)
+ Have: is_finite_f64(a_1).
+ (* Assertion *)
+ Have: of_f64(a_1) = r.
+}
+Prove: lt_f64(a_1, b) <-> (r < of_f64(b)).
+
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_acsl/float_compare.i, line 62):
+Assume { (* Pre-condition *) Have: is_finite_f32(a) /\ is_finite_f64(b). }
+Prove: is_finite_f64(to_f64(of_f32(a))).
+
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_acsl/float_compare.i, line 63):
+Let r = of_f32(a).
+Let a_1 = to_f64(r).
+Assume {
+ (* Pre-condition *)
+ Have: is_finite_f32(a) /\ is_finite_f64(b).
+ (* Assertion *)
+ Have: is_finite_f64(a_1).
+}
+Prove: of_f64(a_1) = r.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function cmp_ff
+------------------------------------------------------------
+
+Goal Post-condition 'DEF' in 'cmp_ff':
+Assume { (* Pre-condition *) Have: is_finite_f32(a) /\ is_finite_f32(b). }
+Prove: (if lt_f32b(a, b) then 1 else 0)
+ = (if (of_f32(a) < of_f32(b)) then 1 else 0).
+
+------------------------------------------------------------
+
+Goal Post-condition 'REL1' in 'cmp_ff':
+Assume { (* Pre-condition *) Have: is_finite_f32(a) /\ is_finite_f32(b). }
+Prove: lt_f32(a, b) <-> (of_f32(a) < of_f32(b)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'REL2' in 'cmp_ff':
+Assume { (* Pre-condition *) Have: is_finite_f32(a) /\ is_finite_f32(b). }
+Prove: lt_f32(a, b) <-> (of_f32(a) < of_f32(b)).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function cmp_fnan
+------------------------------------------------------------
+
+Goal Post-condition 'POS' in 'cmp_fnan':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition 'NEG' in 'cmp_fnan':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
index d0b001c2edc097127a4258a4203f7296d3b6ecd4..968431f963b05d789b5f1558c6ae2e16227fddce 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
@@ -2,17 +2,39 @@
[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
-[wp] 4 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare_greater : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_test_float_compare : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_test_float_compare_greater : Valid
-[wp] Proved goals: 4 / 4
- Qed: 0
- Alt-Ergo: 4
+[wp] Warning: Missing RTE guards
+[wp] 19 goals scheduled
+[wp] [alt-ergo] Goal typed_lemma_finite_32_64 : Valid
+[wp] [alt-ergo] Goal typed_lemma_finite_32_64_real : Unsuccess
+[wp] [alt-ergo] Goal typed_lemma_test_double_compare : Valid
+[wp] [alt-ergo] Goal typed_lemma_test_double_compare_greater : Valid
+[wp] [alt-ergo] Goal typed_lemma_test_float_compare : Valid
+[wp] [alt-ergo] Goal typed_lemma_test_float_compare_greater : Valid
+[wp] [alt-ergo] Goal typed_cmp_dd_ensures_DEF : Valid
+[wp] [alt-ergo] Goal typed_cmp_dd_ensures_REL1 : Valid
+[wp] [alt-ergo] Goal typed_cmp_dd_ensures_REL2 : Valid
+[wp] [alt-ergo] Goal typed_cmp_fd_ensures_DEF : Valid
+[wp] [alt-ergo] Goal typed_cmp_fd_ensures_REL1 : Valid
+[wp] [alt-ergo] Goal typed_cmp_fd_ensures_REL2 : Valid
+[wp] [alt-ergo] Goal typed_cmp_fd_assert : Valid
+[wp] [alt-ergo] Goal typed_cmp_fd_assert_2 : Valid
+[wp] [alt-ergo] Goal typed_cmp_ff_ensures_DEF : Valid
+[wp] [alt-ergo] Goal typed_cmp_ff_ensures_REL1 : Valid
+[wp] [alt-ergo] Goal typed_cmp_ff_ensures_REL2 : Valid
+[wp] [Qed] Goal typed_cmp_fnan_ensures_POS : Valid
+[wp] [Qed] Goal typed_cmp_fnan_ensures_NEG : Valid
+[wp] Proved goals: 18 / 19
+ Qed: 2
+ Alt-Ergo (why3): 16 (unsuccess: 1)
[wp] Report in: 'tests/wp_acsl/oracle_qualif/float_compare.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/float_compare.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
-Lemma - 4 (28..40) 4 100%
+Lemma - - 6 83.3%
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+cmp_ff - - 3 100%
+cmp_dd - - 3 100%
+cmp_fd - - 5 100%
+cmp_fnan 2 - 2 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
index ac5a52640069fe4f37d2173e5c5c77778a44fa53..2ba23416456faa39cde87569f6ab9693ef9bc593 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
@@ -17,7 +17,7 @@
[wp] [Qed] Goal typed_g_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_g_assigns_normal_part3 : Valid
[wp] [Qed] Goal typed_unreachable_smt_with_contract_ensures_ok_2 : Valid
-[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_requires_ok : Valid
+[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_2_requires_ok : Valid
[wp] Proved goals: 8 / 8
Qed: 8
[wp] Report in: 'tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.0.report.json'
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
index e18208021ccb21482035e39a7353f2c3dcf98688..98ab24cc12de61c5d5ae89cbc5e7f47c915dc1c0 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
@@ -65,7 +65,7 @@
[wp] [Qed] Goal typed_ref_call_ref_valid_assigns_normal_part4 : Valid
[wp] [Qed] Goal typed_ref_call_ref_valid_assigns_normal_part5 : Valid
[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_requires : Valid
-[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_requires : Valid
+[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_2_requires : Valid
[wp] [Qed] Goal typed_ref_call_two_ref_ensures : Valid
[wp] [Qed] Goal typed_ref_call_two_ref_assigns_exit_part1 : Valid
[wp] [Qed] Goal typed_ref_call_two_ref_assigns_exit_part2 : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
index 5bfd4b969d1181a464dfba7b4c2af80db87bcd2d..03d5b7f2fd3a7dcd17af11e41b87908e51636da0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
@@ -5,7 +5,7 @@
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
[wp] [Qed] Goal typed_f_call_g_requires : Valid
-[wp] [Qed] Goal typed_f_call_g_requires : Valid
+[wp] [Qed] Goal typed_f_call_g_2_requires : Valid
[wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok_2 : Valid
[wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok_3 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
index 8676944fb53b5219663b759b05710eb35ea5ee66..2a297e0ebefb2b37d8791372db2d79f4f853723e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
@@ -8,19 +8,19 @@
[wp] [Alt-Ergo] Goal typed_caller_ensures_P1 : Valid
[wp] [Alt-Ergo] Goal typed_caller_ensures_P2 : Valid
[wp] [Alt-Ergo] Goal typed_caller_call_job_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller_call_job_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller_call_job_2_requires : Valid
[wp] [Qed] Goal typed_caller2_ensures_K : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_Q1 : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_Q2 : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_R : Valid
[wp] [Alt-Ergo] Goal typed_caller2_call_job2_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller2_call_job2_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller2_call_job2_2_requires : Valid
[wp] [Qed] Goal typed_caller3_ensures_K : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_Q1 : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_Q2 : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_R : Valid
[wp] [Alt-Ergo] Goal typed_caller3_call_job3_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller3_call_job3_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller3_call_job3_2_requires : Valid
[wp] [Qed] Goal typed_job_ensures_K : Valid
[wp] [Qed] Goal typed_job_ensures_P : Valid
[wp] [Qed] Goal typed_job_assigns_part1 : Valid
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 2cde75506a5960e32eb8a2e6493738a24241bedb..894def5654e6c88349bb8a1f22669a3cf852d950 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -232,22 +232,27 @@ module PropId =
(* --- Lagacy Naming --- *)
(* -------------------------------------------------------------------------- *)
-module LegacyNames :
+module NameUniquify(D:Datatype.S_with_collections)(S:sig
+ val name: string
+ val basename: D.t -> string
+ end) :
sig
- val get_prop_id_name: prop_id -> string
-end = struct
+ val unique_basename: D.t -> string
+end
+=
+struct
module NamesTbl = State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
(struct
- let name = "WpPropertyNames"
+ let name = S.name^"Names"
let dependencies = [ ]
let size = 97
end)
module IndexTbl =
- State_builder.Hashtbl(PropId.Hashtbl)(Datatype.String)
+ State_builder.Hashtbl(D.Hashtbl)(Datatype.String)
(struct
- let name = "WpPropertyIndex"
+ let name = S.name^"Index"
let dependencies =
[ Ast.self;
NamesTbl.self;
@@ -258,6 +263,38 @@ end = struct
let size = 97
end)
+
+ (** returns the name that should be returned by the function [get_prop_name_id]
+ if the given property has [name] as basename. That name is reserved so that
+ [get_prop_name_id prop] can never return an identical name. *)
+ let reserve_name_id pid =
+ let basename = S.basename pid in
+ try
+ let speed_up_start = NamesTbl.find basename in
+ (* this basename is already reserved *)
+ let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
+ in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
+ unique_name
+ with Not_found -> (* first time that basename is reserved *)
+ NamesTbl.add basename 2 ;
+ basename
+
+ (** returns a unique name identifying the property.
+ This name is built from the basename of the property. *)
+ let unique_basename pid =
+ try IndexTbl.find pid
+ with Not_found -> (* first time we are asking for a name for that [ip] *)
+ let unique_name = reserve_name_id pid in
+ IndexTbl.add pid unique_name ;
+ unique_name
+
+end
+
+module LegacyNames :
+sig
+ val get_prop_id_name: prop_id -> string
+end = struct
+
let base_id_prop_txt = Property.LegacyNames.get_prop_name_id
let basename_of_prop_id p =
@@ -296,29 +333,17 @@ end = struct
Printf.sprintf "%s_part%06d" basename (succ k)
in normalize_basename basename
- (** returns the name that should be returned by the function [get_prop_name_id]
- if the given property has [name] as basename. That name is reserved so that
- [get_prop_name_id prop] can never return an identical name. *)
- let reserve_name_id pid =
- let basename = get_prop_id_basename pid in
- try
- let speed_up_start = NamesTbl.find basename in
- (* this basename is already reserved *)
- let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
- in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
- unique_name
- with Not_found -> (* first time that basename is reserved *)
- NamesTbl.add basename 2 ;
- basename
+
+ module UniquifyPropId = NameUniquify(PropId)(struct
+ let name = "WpProperty"
+ let basename = get_prop_id_basename
+ end)
+
(** returns a unique name identifying the property.
This name is built from the basename of the property. *)
let get_prop_id_name pid =
- try IndexTbl.find pid
- with Not_found -> (* first time we are asking for a name for that [ip] *)
- let unique_name = reserve_name_id pid in
- IndexTbl.add pid unique_name ;
- unique_name
+ UniquifyPropId.unique_basename pid
end
@@ -332,45 +357,27 @@ sig
end =
struct
- module NamesTbl = State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
- (struct
- let name = "Wp.WpPropId.Names.NamesTbl"
- let dependencies = [ ]
- let size = 97
- end)
-
- module IndexTbl =
- State_builder.Hashtbl(Property.Hashtbl)(Datatype.String)
- (struct
- let name = "Wp.WpPropId.Names.IndexTbl"
- let dependencies =
- [ Ast.self;
- NamesTbl.self;
- Globals.Functions.self;
- Annotations.code_annot_state;
- Annotations.funspec_state;
- Annotations.global_state ]
- let size = 97
- end)
-
- let compute_ip ip =
- let truncate = max 20 (Wp_parameters.TruncPropIdFileName.get ()) in
- let basename = Property.Names.get_prop_basename ~truncate ip in
- try
- let speed_up_start = NamesTbl.find basename in
- let n,unique_name = Extlib.make_unique_name
- NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
- in NamesTbl.replace basename (succ n) ;
- unique_name
- with Not_found -> (* first time that basename is reserved *)
- NamesTbl.add basename 2 ; basename
+ (** Uniquify the first part of the prop_id *)
+ module Uniquify1 = NameUniquify(Property)(struct
+ let name = "Wp.WpPropId.Names."
+ let basename ip =
+ let truncate = max 20 (Wp_parameters.TruncPropIdFileName.get ()) in
+ Property.Names.get_prop_basename ~truncate ip
+ end)
let get_ip ip =
- try IndexTbl.find ip
- with Not_found -> (* first time we are asking for a name for that [ip] *)
- let unique_name = compute_ip ip in
- IndexTbl.add ip unique_name ;
- unique_name
+ Uniquify1.unique_basename ip
+
+ (** Uniquify call-site for precondition check. So
+ that precondition of the same call-site are grouped *)
+ module CallSite = Datatype.Triple_with_collections
+ (Kernel_function)(Kernel_function)(Stmt)
+ (struct let module_name = "Wp.WpPropId.CallSite" end)
+ module Uniquify_Stmt = NameUniquify(CallSite)(struct
+ let name = "Wp.WpPropId.Names3."
+ let basename (caller_kf,callee_kf,_stmt) =
+ (Kernel_function.get_name caller_kf)^"_call_"^(Kernel_function.get_name callee_kf)
+ end)
let get_prop_id_base p =
match p.p_kind , p.p_prop with
@@ -381,13 +388,22 @@ struct
| PKVarPos , p -> get_ip p ^ "_positive"
| PKAFctOut , p -> get_ip p ^ "_normal"
| PKAFctExit , p -> get_ip p ^ "_exit"
- | PKPre(_kf,stmt,pre) , _ ->
- let kf_name_of_stmt =
- Kernel_function.get_name
- (Kernel_function.find_englobing_kf stmt)
- in Printf.sprintf "%s_call_%s" kf_name_of_stmt (get_ip pre)
+ | PKPre(callee_kf,stmt,pre) , _ ->
+ let caller_kf = Kernel_function.find_englobing_kf stmt in
+ let call_string =
+ Uniquify_Stmt.unique_basename (caller_kf,callee_kf,stmt)
+ in
+ (** remove name of callee kernel function given by get_ip *)
+ let ip_string = get_ip pre in
+ let ip_string =
+ Extlib.opt_conv ip_string
+ (Extlib.string_del_prefix
+ ((Kernel_function.get_name callee_kf)^"_")
+ ip_string)
+ in
+ call_string^"_"^ip_string
- let get_prop_id_name p =
+ let get_prop_id_basename p =
let basename = get_prop_id_base p in
match p.p_part with
| None -> basename
@@ -397,6 +413,14 @@ struct
if n < 1000 then Printf.sprintf "%s_part%03d" basename (succ k) else
Printf.sprintf "%s_part%06d" basename (succ k)
+ module Uniquify2 = NameUniquify(PropId)(struct
+ let name = "Wp.WpPropId.Names2."
+ let basename = get_prop_id_basename
+ end)
+
+ let get_prop_id_name p =
+ Uniquify2.unique_basename p
+
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 782b9a5425dfb48bfc7d165900d6733b75a2b27b..90d1fd2dbd29a70d99de4594de954babd0ef4af6 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -109,7 +109,6 @@ struct
| Qed -> "qed"
| AltErgo -> "mlw"
| Why3 _ -> "why"
- | Why3ide -> "why"
| Coq -> "v"
| Tactical -> "tac"
in
@@ -121,7 +120,6 @@ struct
| Qed -> "qed"
| AltErgo -> "mlw"
| Why3 _ -> "why"
- | Why3ide -> "why"
| Coq -> "v"
| Tactical -> "tac"
in
@@ -539,7 +537,7 @@ struct
match r.verdict with VCS.Computing _ -> false | _ -> true
let class_of_prover = function
- | Qed | Tactical | AltErgo | Coq | Why3ide -> None
+ | Qed | Tactical | AltErgo | Coq -> None
| Why3 dp ->
let cp =
try String.sub dp 0 (String.index dp ':')