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

  • Subject: [Frama-c-discuss] Frama-C doesn't warn me about the illegal assignment of a variable
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
  • Date: Tue, 8 Dec 2009 16:48:20 +0100
  • In-reply-to: <7F579E29361D4048A9316F38A9D017EC367E17C356@EkkyoExch1.ekkyo.local>
  • References: <7F579E29361D4048A9316F38A9D017EC367E17C356@EkkyoExch1.ekkyo.local>
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/fe09659f/attachment.htm