Frama-C-discuss mailing list archives

Pascal.CUOQ at cea.fr (CUOQ Pascal) · Tue, 21 Apr 2009 19:31:06 -0000

Please find here an excerpt from the upcoming documentation.
The whole 60 pages of the manual will be available soon.

The two messages that you stumbled upon should be
considered to be in category either "loss of precision message"
or "progress message" depending on what you are trying to do.
If you are trying to analyse a deterministic execution while
remaining as precise as an actual execution would, they indicate
where the analyzer is first failing to keep with your objective
(hint: use either "-slevel 12" or "-ulevel 12").
If you are not trying to be as precise as an execution
(for instance because you introduced non-determinism on
purpose), they should be considered as progress messages.

Pascal

\section{Log messages emitted by the value analysis}

This section categorizes the messages displayed by the value analysis
in the batch version of the analyzer (\lstinline|frama-c|).
When using the graphical interface (\lstinline|frama-c-gui|), the messages
are intercepted and directed to different panels for easier access.

\subsection{Results}

With the batch version of Frama-C,
the results of the computations are displayed on the standard output.
For some computations, the information computed
can not easily be represented in a human-readable way. In this case, 
it is not displayed at all, and can only be accessed through the
GUI or programmatically. In other cases, a compromise had to
be reached. For instance, although variation domains for variables
are available for any point in the execution of the analyzed application,
the batch version only displays, for each function, the values that
hold whenever the end of this function is reached.

\subsection{Proof obligations}\label{obligations}

The correctness of the results provided by the value analysis
is guaranteed only if the user verifies all the
proof obligations generated during the analysis.
In the current version of Frama-C, these proof obligations
are displayed as messages that start with \lstinline|Warning:...|
and contains either the word \lstinline|alarm| or \lstinline|assert|.
Frama-C comes with a common specification language for all plug-ins,
called ACSL (\url{http://www.frama-c.cea.fr/acsl.html}).
Most of the proof obligations emitted by the value analysis
are expressed in ACSL.
Each proof obligation message contains
the nature and the origin of the obligation.

It is also possible to obtain a version of the analyzed source
code annotated with the proofs obligations. Please note that the proof
obligations that are not yet expressed in ACSL are missing
from the output source code. For those alarms which are expressed
as ACSL assertions, do also note that 
while ACSL's syntax is used, the value analysis's support for
ACSL is still partial in the sense that some explicit coercion
operations may be missing
from these formulas to make them express correctly in ACSL
the condition that ensures the absence of error. This bug will be
fixed in a later version.

[list of alarms skipped]

\subsection{Experimental status messages}

Some messages may warn that a feature is experimental.
This means that a part of the analyzer that gets used during
the analysis is less tested or is known to have issues.
An example of such a message is:
\begin{logs}
Warning: float support is experimental
\end{logs}

\subsection{Informational messages regarding the loss of precision}

Some messages may warn that the analysis is making an operation likely
to cause a loss of precision.  These messages are not proof
obligations and it is not mandatory for the user to act on them. They
are intended to help the user trace the results of the analysis, and
give as much information as possible in order to help 
em\footnote{Spivak pronouns are used throughout this manual:
\url{http://en.wikipedia.org/wiki/Spivak_pronoun}‌} find
when the analysis becomes imprecise.
These messages are only useful when it is important to analyze the application
with precision. The value analysis remains correct even when it
is imprecise.
\medskip

Examples of such messages are:
\begin{logs}
val9.c:10: Warning: assigning non deterministic value for the first time

origin.c:102: Warning: assigning imprecise value to q2.
 The imprecision originates from Misaligned {origin.c:102;}

origin.c:102: Warning: extracting bits of a pointer

origin.c:102:
Warning: reading left-value *((int **)((char *)(v.t) + 3)).
The location is {‌{ v -> {88; } ;}‌}.
It contains a garbled mix of {y; }
because of Arithmetic {tests/misc/origin.c:102; }.
\end{logs}

\subsection{Progress messages}

Some messages are only intended to inform the user of the progress of
the analysis. Here are examples of such messages:
\begin{logs}
Parsing

[preprocessing] running gcc -C -E -I.   tests/misc/alias.c

[values] computing for function f <-main
[values] called from tests/misc/alias.c:46

[values] Recording results for f

[values] done for function f
\end{logs}

Progress messages
are informational only. If you find the analysis fast enough, there is no
reason to read them at all. If it seems too slow, these messages can help
find where time is spent.

-----Original Message-----
From: frama-c-discuss-bounces at lists.gforge.inria.fr on behalf of Hollas Boris (CR/AEY1)
Sent: Tue 4/21/2009 4:39 PM
To: 'Frama-C public discussion'
Subject: [Frama-c-discuss] Value analysis emits warning for for-loop

Hi,

run on code [1], the value analysis plugin emits warnings [2] that I don't understand:
- why does frama-c warn about entering the for-loop for the first time?
- why does it warn about the assignment i=0?

-Boris

[1]

void main() {
  int i;

  for(i=0; i<10; i++) ;
}

[2]

tst8.c:4: Warning: entering loop for the first time
tst8.c:4: Warning: assigning non deterministic value for the first time

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss