Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C doesn't warn me about the illegal assignment of a variable

Boris, Pascal, thanks for your answers.

For my starting with this tool, I was benching my understanding and the use of the tool with a GUI approach and little samples (more understandable).
But with your comments, I will do a benchmark with batch versions and automatic extraction.

...
Otherwise, thanks for the development team of Frama-C that give a development way to do a safe code!

Sincerely,
Damien


De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Pascal Cuoq
Envoy? : mardi 8 d?cembre 2009 16:48
? : Frama-C public discussion
Objet : [Frama-c-discuss] Frama-C doesn't warn me about the illegal assignment of a variable

Hello,

I am working on the command "@ assigns \nothing". See my sample code below:
########################################
/*@ assigns \nothing;
*/
void Compte_heure (unsigned int *fHeure)
{
                *fHeure = (*fHeure)+1;
}
########################################

I want that Frama-C warns me about the non-wanted assignment of the variable "*fHeure".

This seems like a proper way to use Frama-C.


My command line with Frama-C is "frama-c-gui -slevel 15 -val *.c"

This won't help for the following reasons:

* the value analysis (started by -val) needs an entry point (it defaults to function "main"
if there is one). Using it on single functions out of context is slightly more advanced
but your function above is simple enough for it to work: use options "-lib-entry -main Compte_heure"
in addition to "-val". The value analysis then generates a non-aliasing calling context
in which it analyses the function (here, an implicit unsigned int array star_fHeure
to which fHeure points.

* the value analysis is not able to check that functions implement assigns clauses
correctly. It can, however, display its own view (in its own, slightly different format)
of what the function is doing, that you can manually compare to your expectations.

You can use the command-line "frama-c -val -lib-entry -main Compte_heure t.c -deps"
and notice that
[from] Function Compte_heure:
         star_fHeure[0] FROM fHeure; star_fHeure[0]; (and default:false)
denotes an assignment to star_fHeure[0] which is not what you expected,
or use "frama-c -val -lib-entry -main Compte_heure t.c -out"
and notice that
[value] Out (internal) for function Compte_heure:
          star_fHeure[0];
is not what you expected.

There are subtle differences between -deps and -out that are
documented in the Value Analysis manual and that have to do with
execution paths that do not terminate.

I guess you will find this unsatisfying because you would rather write
the specification first and have the tool check that what you have written
is true. If you want this kind of workflow, Jessie is your best bet.

 If I use "Fraam-C" with the plugin "Jessie" and the automatic code checker "Alt-Ergo", there is a warning for the assignment of the variable "*fHeure".
My command line with Frama-C is "frama-c -jessie-gui -jessie-analysis -jessie-atp simplify *.c ?

Jessie specialists should confirm this, but I think the warning you obtain
should be interpreted as meaning that the specification you provided is
indeed not satisfied. Isn't this what you expected?

Do you know the way to have the warning statement displayed in Frama-C ?

This is the way the tools are integrated for now. Even for -deps and -out,
I am not sure where the results can be found in the GUI because this
is something which is changing at the moment in the development version.
Once they have appropriated the tools, our industrial users end up
relying mostly on the batch versions and automatic extraction of the
information they are interested in from the logs anyway. The GUI is
not finished but we are working on it...

Pascal

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091208/f087f0f7/attachment.htm