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] annotations and value analysis

>  I guess it will be same with output parameters of the function  
> (gest_index(int cmd, int* pindex). Can you confirm ?

If you mean adding respectively:

   @ ensures  *p >= 10 ;
...
int get_index(int /* in */ cmd, int *p)
...
   get_index(x, &R);

It is already supported:

[value] Values for function main:
           R ? [10..199]


> And what about annotation on declaration of the function without  
> definition?

In this case you *need* an assigns clause in the function contract.
You can use dependencies (\from ...), the extension described at
page 56 of the currently distributed ACSL documentation.

The assigns clause with dependencies is interpreted
by the value analysis, but at this time, the pre- and
post-conditions are not.

The policy is that announcement of features and dates is not
allowed on this mailing-list
(as per http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-November/000780.html 
  )
and therefore, since I would never go against one of
this mailing list's official policy,
I can't have promised support for \result soon.
Similarly I can't comment on the availability of support for
pre- and post-conditions in library function specifications
in the value analysis.

Pascal

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