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



Dear Frama-C users,

I am using "Frama-C" for the first time and I am doing some test cases to know if my use of this tool is OK.

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".
My command line with Frama-C is "frama-c-gui -slevel 15 -val *.c"

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 >

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

Thanks,

Best regards,
Damien

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091208/c67ee4c8/attachment-0001.htm