--- layout: fc_discuss_archives title: Message 85 from Frama-C-discuss on December 2009 ---
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