--- layout: fc_discuss_archives title: Message 83 from Frama-C-discuss on December 2009 ---
Damien Vidal wrote: > > 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 not use both jessie-gui and "-jessie-atp simplify" If you used the last version of Frama-C, this would be impossible (-jessie-gui disappeared) > Do you know the way to have the warning statement displayed in Frama-C ? > The jessie plugin will not directly display the warning in Frama-C gui but in its own gui. frama-c -jessie-gui -jessie-analysis *.c or with beryllium 2: frama-c -jessie *.c will do it - Claude > > Thanks, > > Best regards, > > Damien > > ------------------------------------------------------------------------ > > _______________________________________________ > 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 -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |